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

Modeling and Verification of Cyber-physical Systems Based on Timed Automata

作　　者：陈志辉[1] 

机构地区：[1]莆田学院电子信息工程系,福建莆田351100

出　　处：《计算机与现代化》2012年第10期125-130,135,共7页Computer and Modernization

基　　金：国家重点基础研究发展计划(973)项目子课题(2009CB320705);福建省科技项目(2010H6019)

摘　　要：信息物理融合系统的建模和验证是当前研究的一个热点。本文通过分析信息物理融合系统的体系结构,利用时间自动机为建模工具,将该结构中的各个组件分别进行建模,以表现它们的分布性和实时性。这些时间自动机组成一个网络模型,用于刻划整个系统之间的并发通信和协作过程。最后,提出一组该系统要满足的性质(包括时间约束),运用模型检测工具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.Based 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.

关 键 词：信息物理融合系统 时间自动机 模型检测 UPPAAL 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]