本书在对国内外相关研究进行梳理的基础上，第一部分首先阐释了微分动态逻辑及其三种扩展逻辑及其证明演算，第二部分探讨了混成系统的自动定理证明，第三部分是混成系统验证实例研究和应用研究。全书从逻辑分析、数学建模、证明义务和验证技术四个方面展开研究，探讨了空中交管系统、列车控制系统、分布式汽车控制系统的防撞策略，验证了这些系统的安全性、可控性、活性和防撞功能。本书主要从逻辑分析、数学建模、证明义务和验证技术这四个方面开展研究，提出一个全面的精化开发混成系统的方案，提出并论证基于微分不变式的混成模型语言的证明义务，给出混成系统精化开发的预设规则，通过规则证明特定模型的正确性。在深入研究微分动态逻辑及其三种扩展逻辑的基础上，分别把空中交通管制系统、列车控制系统和分布式汽车控制系统的防撞策略作为实际案例进行探讨，验证这些系统的安全性、可控性、活性和防撞功能。

更多科学出版社服务，请扫码获取。