Formal Modelling, Analysis and Verification of Hybrid Systems
Formal Modelling, Analysis and Verification of Hybrid Systems
复制标题
DOI：
10.1007/978-3-642-39721-9_5
复制
发表时间：
2013-08
期刊：
影响因子：
--
通讯作者：
N. Zhan;Shuling Wang;Hengjun Zhao
中科院分区：
文献类型：
--
作者：
N. Zhan;Shuling Wang;Hengjun Zhao
混合系统是嵌入式系统的一种数学模型，被广泛应用于复杂嵌入式系统的设计中。在本章中，我们将介绍我们对混合系统进行形式化建模、分析和验证的系统方法。在我们的框架中，混杂系统用混合CSP(HCSP)建模，并用混合Hoare逻辑(HHL)来描述和推理，HHL是Hoare逻辑对混杂系统的扩展。针对混杂系统的演绎验证，提出了一种完整的多项式混杂系统多项式不变量的生成方法，并实现了HHL的定理证明器，为验证提供了工具支持。我们给出了一些来自现实世界的案例，例如中国三级高速列车控制系统(CTCS-3)。此外，基于我们的不变量生成方法，我们考虑了如何通过归结为约束求解来综合所考虑的混合系统的切换逻辑，以满足给定的安全性、活性、最优性要求或它们的任意组合。我们还讨论了混杂系统的其他问题，例如稳定性分析。
Hybrid systems is a mathematical model of embedded systems, and has been widely used in the design of complex embedded systems. In this chapter, we will introduce our systematic approach to formal modelling, analysis and verification of hybrid systems. In our framework, a hybrid system is modelled using Hybird CSP (HCSP), and specified and reasoned about by Hybrid Hoare Logic (HHL), which is an extension of Hoare logic to hybrid systems. For deductive verification of hybrid systems, a complete approach to generating polynomial invariants for polynomial hybrid systems is proposed; meanwhile, a theorem prover for HHL that can provide tool support for the verification has been implemented. We give some case studies from real world, for instance, Chinese High-Speed Train Control System at Level 3 (CTCS-3). In addition, based on our invariant generation approach, we consider how to synthesize a switching logic for a considered hybrid system by reduction to constraint solving, to meet a given safety, liveness, optimality requirement, or any of their combinations. We also discuss other issues of hybrid systems, e.g., stability analysis.