基于微分动态逻辑的CPS建模与属性验证  

Transforming HybridUML to Hybrid Program for CPS Property Verification

作　　者：朱敏[1] 李必信[1] 陈乔乔[1] 吉顺慧[1] 李加凯[1] 

机构地区：[1]东南大学计算机科学与工程学院,江苏南京211189

出　　处：《电子学报》2012年第6期1126-1132,共7页Acta Electronica Sinica

基　　金：国家自然科学基金(No.60973149);博士点基金(No.20100092110022);中科院计算机科学国家重点实验室开放基金基金(No.SYSKF1110)

摘　　要：随着信息物理融合系统(Cyber-Physical Systems,CPS)应用的越来越普及,CPS的设计和实现能否满足实际需求显得至关重要.本文提出了一种CPS建模与属性验证框架.在框架中,首先使用HybridUML对CPS进行建模,然后将该通用模型转换为形式化模型,进而进行形式化验证.本文采用的形式化验证方法为dL(Differential Dynamic Log-ic),其操作模型为hybrid program.将HybridUML模型转换为hybrid program时,基于语义一致性的原则定义转换规则.转换完成后,结合得到的hybrid program对验证的CPS属性进行规约,最后使用定理证明器KeYmaera对属性进行自动化验证.With the wide application of cyberphysical systems（CPS）, it is of vital importance to ensure that the design and implementation of CPS meet critical performance requirements （e. g., security, reliability）. This paper presents a framework for CPS modeling and verification. In the framework, CPS are modelled by HybridUML and then the genetic model is transformed to a for real model that is suitable for reasoning with the help of formal methods. The fomaal method adopted is differential dynamic logic （dL） whose operational model is hybrid program（liP）.When transforming a HybridUML model to its corresponding HP presentalion, transformation rules are defined according to semantic consistency. After transformation, CPS properties are specified on the ba sis of the resulting HP, and finally, the properties are automatically verified through the theorem prover KeYmaera.

关 键 词：信息物理融合系统 微分动态逻辑 HybridUML 模型转换 验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]