本书聚焦于高可靠动态系统的形式化设计与验证研究，提出了一种形式化描述与验证方法，主要对利用可执行时序逻辑语言XYZ／RE来精确描述系统、XYZ／RE到时间自动机的映射规则的建立、嵌入式动态系统的建模等进行了详细介绍，并对借助基于时间自动机的验证工具UPPAAL对系统进行形式化验证，以提高系统的正确性、可靠性、可信度等进行了讲解。此外，本书结合智能制造、智能家居等典型场景开展实证，并提出在进行工业控制动态系统设计时可融入先进测试技术的理念，同时介绍了动态系统的质量保证方法。 本书可为物联网、智能制造等领域高可靠动态系统设计的相关研究人员提供方法参考。

第1章 绪论
1.1 研究背景
1.2 研究现状
1.3 研究内容
1.4 本书结构
第2章 理论基础
2.1 动态系统
2.2 形式化方法
2.3 XYZ子语言XYZ/RE
2.4 本章小结
第3章 基于时间自动机的验证方法
3.1 时间自动机
3.2 自动验证工具UPPAAL
3.3 本章小结
第4章 XYZ/RE到时间自动机的映射
4.1 对XYZ/RE的扩展和约束
4.2 XYZ/RE到时间自动机的映射规则
4.3 本章小结
第5章 家居生活动态系统的描述及验证
5.1 煤气炉控制系统
5.2 咖啡机控制系统
5.3 本章小结
第6章 嵌入式动态系统的建模与验证
6.1 嵌入式动态系统概述
6.2 燃气报警器结构
6.3 燃气报警器系统建模
6.4 本章小结
第7章 工业控制动态系统的建模与验证
7.1 工业控制动态系统概述
7.2 生产线系统结构
7.3 生产线系统建模
7.4 本章小结
第8章 动态系统的质量保证方法
8.1 动态系统的质量保证方法概述
8.2 基于谓词的系统需求测试用例生成方法
8.3 大数据测试方法
8.4 本章小结
第9章 总结与展望
9.1 总结
9.2 展望
参考文献