基于时空自动机的CPS建模与验证

Modeling and Verification of CPS Based on Spatial Hybrid Automata

为了描述信息物理融合系统(cyber-physical systems,CPS)的时空一致性,一种实时规范语言STe C已经提出[1],CPS的设计和实现能否满足时空一致性显得十分重要。文中对混成自动机进行了扩展,提出了具有位置驱动特点的时空自动机。文中提出了基于时空自动机的CPS建模与验证框架。在框架中,首先使用STe C语言对CPS进行了描述并使用时空自动机对CPS进行建模。文中采用的形式化验证方法为微分动态逻辑(differential dynamic logic,DL),其操作模型为HP(hybrid program)。利用DL可以将所建模型转换为对应的HP。结合得到的HP对验证的CPS属性进行规约,最后使用定理证明器Ke Ymaera对属性进行自动化验证。

In order to describe the requirement of spatial and temporal consistence of cyber- physicalsystems （CPS）, a specification language called STeC was proposed by Chen [1]. It is of vital importance toensure that the design and implementation of CPS meet the requirement of spatial and temporalconsistence. The Spatial Hybrid Automata （SHA）, characteristic of the location-triggered, is proposedbased on the extended hybrid automata. This paper presents a framework of CPS modeling andverification based on SHA, where CPS are described by STeC and modeled by SHA. The adopted formalmethod is the differential dynamic logic （DL）, whose the operational model is Hybrid Program （HP）. TheSHA model is transformed to its corresponding HP through DL. Then CPS properties are specified basedon the result from HP. Finally, the CPS properties are automatically verified through the theorem-provernamed KeYmaera.