基于时间自动机的信息物理融合系统建模与验证

摘要

信息物理融合系统的建模和验证是当前研究的一个热点.本文通过分析信息物理融合系统的体系结构,利用时间自动机为建模工具,将该结构中的各个组件分别进行建模,以表现它们的分布性和实时性.这些时间自动机组成一个网络模型,用于刻划整个系统之间的并发通信和协作过程.最后,提出一组该系统要满足的性质(包括时间约束),运用模型检测工具UPPAAL自动验证本系统的正确性.%At present, the modeling and verification of Cyber-physical Systems(CPS) is becoming a hot topic of CPS software design. First, a typical prototype of CPS architecture is given and it generally consists of several basic components, e. G. , sensors, actuators, etc. Baaed on timed automata, CPS modeling approach is proposed, in which these components are modeled as individual timed automata reflecting their distributed and real-time characteristics. Then, all these time automata come into a network that represents concurrent communication and collaboration of the whole CPS. Finally, some properties (including time constraints) with the CPS are presented, and the correctness of the whole system is automatically verified by using the model-checking tool UPPAAL.