【摘要】 为了描述信息物理融合系统(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对属性进行自动化验证。更多还原

【Abstract】 In order to describe the requirement of spatial and temporal consistence of cyber- physical systems(CPS), a specification language called STe C was proposed by Chen [1]. It is of vital importance to ensure that the design and implementation of CPS meet the requirement of spatial and temporal consistence. The Spatial Hybrid Automata(SHA), characteristic of the location-triggered, is proposed based on the extended hybrid automata. This paper presents a framework of CPS modeling and verification based on SHA, where CPS are described by STe C and modeled by SHA. The adopted formal method is the differential dynamic logic(DL), whose the operational model is Hybrid Program(HP). The SHA model is transformed to its corresponding HP through DL. Then CPS properties are specified based on the result from HP. Finally, the CPS properties are automatically verified through the theorem-prover named Ke Ymaera.更多还原