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

作     者：赵文明 陈仪香 张敏 Zhao Wenming;Chen Yixiang;Zhang Min

作者机构：杭州职业技术学院信息电子系杭州310018 华东师范大学教育部软硬件协同设计技术与应用工程研究中心上海200062 华东师范大学上海市高可信计算重点实验室上海200062 

基　　金：国家"973"重点基础研究发展计划项目基金(2011CB302802) 

出 版 物：《科技通报》 (Bulletin of Science and Technology)

年 卷 期：2015年第31卷第1期

页      码：94-99页

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

主 题 词：时空自动机 CPS 微分动态逻辑 时空一致性 验证 KeYmaera 

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 08[工学] 081201[081201] 0812[工学-测绘类] 

D　O　I：10.13774/j.cnki.kjtb.2015.01.022

馆 藏 号：203925893...