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