摘要
随着信息物理融合系统(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.
出处
《电子学报》
EI
CAS
CSCD
北大核心
2012年第6期1126-1132,共7页
Acta Electronica Sinica
基金
国家自然科学基金(No.60973149)
博士点基金(No.20100092110022)
中科院计算机科学国家重点实验室开放基金基金(No.SYSKF1110)
