物联网交互系统的量化验证方法研究
| 摘要 | 第5-7页 |
| abstract | 第7-9页 |
| 主要命名中英对照表 | 第15-16页 |
| 主要标号说明 | 第16-17页 |
| 主要符号索引 | 第17-19页 |
| 第一章 绪论 | 第19-29页 |
| 1.1 研究背景与动机 | 第19-22页 |
| 1.2 研究现状与相关工作 | 第22-25页 |
| 1.3 本文工作与主要创新点 | 第25-26页 |
| 1.4 组织结构 | 第26-27页 |
| 1.5 本章小结 | 第27-29页 |
| 第二章 预备知识 | 第29-43页 |
| 2.1 数学符号 | 第29-30页 |
| 2.2 概率理论 | 第30-31页 |
| 2.3 形式化模型Reo | 第31-34页 |
| 2.4 约束自动机理论 | 第34-40页 |
| 2.5 时态逻辑 | 第40-41页 |
| 2.6 本章小结 | 第41-43页 |
| 第三章 物联网交互系统模型 | 第43-65页 |
| 3.1 引言 | 第43-44页 |
| 3.2 代价概率时间Reo模型 | 第44-46页 |
| 3.3 代价概率时间约束自动机 | 第46-58页 |
| 3.4 代价概率时间约束自动机语义 | 第58-63页 |
| 3.4.1 概率时间系统 | 第58-61页 |
| 3.4.2 自动机语义 | 第61-63页 |
| 3.5 本章小结 | 第63-65页 |
| 第四章 物联网交互系统性质规范 | 第65-89页 |
| 4.1 代价概率时间数据流逻辑 | 第65-69页 |
| 4.2 代价概率时间数据流逻辑解释 | 第69-77页 |
| 4.2.1 逻辑解释 | 第71-72页 |
| 4.2.2 模型性质可满足性 | 第72-73页 |
| 4.2.3 逻辑表达能力分析 | 第73-76页 |
| 4.2.4 一体化还是组合化的逻辑依据 | 第76-77页 |
| 4.3 工具自动化验证 | 第77-87页 |
| 4.3.1 pPTCA的简化模型 | 第79-80页 |
| 4.3.2 支持动作集的STA模型 | 第80-84页 |
| 4.3.3 spPTCA到MSTA的转换 | 第84-87页 |
| 4.4 本章小结 | 第87-89页 |
| 第五章 模型行为等价研究 | 第89-135页 |
| 5.1 强互摸拟研究 | 第89-96页 |
| 5.1.1 经典强互模拟 | 第90-91页 |
| 5.1.2 代价约束的强互摸拟 | 第91-94页 |
| 5.1.3 代价约束的强概率互模拟 | 第94-96页 |
| 5.2 弱互摸拟研究 | 第96-122页 |
| 5.2.1 概率模型 | 第97-101页 |
| 5.2.2 经典弱概率互模拟 | 第101-105页 |
| 5.2.3 定性保发散弱互摸拟 | 第105-106页 |
| 5.2.4 定性保等价发散弱互模拟 | 第106-114页 |
| 5.2.5 定量保发散弱互模拟 | 第114-120页 |
| 5.2.6 概率系统与非概率系统一致性 | 第120-122页 |
| 5.3 最大保发散弱互模拟的计算算法 | 第122-133页 |
| 5.3.1 定性保等价发散弱互模拟的判定算法 | 第123-127页 |
| 5.3.2 最大定性保等价发散弱互模拟的计算算法 | 第127-133页 |
| 5.4 本章小结 | 第133-135页 |
| 第六章 应用案例分析 | 第135-149页 |
| 6.1 野外工作站物联网交互系统建模 | 第135-144页 |
| 6.1.1 物理场景需求分析 | 第135-136页 |
| 6.1.2 物联网交互系统建模 | 第136-144页 |
| 6.2 野外工作站物联网交互系统性质分析 | 第144-147页 |
| 6.2.1 升级前的系统 | 第144-146页 |
| 6.2.2 升级后的系统 | 第146-147页 |
| 6.3 本章小结 | 第147-149页 |
| 第七章 总结与展望 | 第149-153页 |
| 7.1 本文工作总结 | 第149-151页 |
| 7.2 后续工作展望 | 第151-153页 |
| 参考文献 | 第153-162页 |
| 致谢 | 第162-164页 |
| 发表论文和科研情况 | 第164-165页 |
