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

作者：赵文明; 陈仪香; 张敏

来源：科技通报, 2015, 31(01): 94-99.

DOI：10.13774/j.cnki.kjtb.2015.01.022

• 时空自动机
• CPS
• 微分动态逻辑
• 时空一致性
• 验证
• KeYmaera

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

• 单位
  杭州职业技术学院; 华东师范大学