一种基于微分代数动态逻辑的CPS建模与验证方法  

A Modeling and Verification Method of CPS Based on Differential-Algebraic Dynamic Logic

作　　者：陈乔乔[1] 李必信[1] 吉顺慧[1] 

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

出　　处：《计算机研究与发展》2013年第4期700-710,共11页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60973149);高等学校博士学科点专项科研基金项目(20100092110022);江苏省高校科研成果产业化推进项目(JHB2011-3)

摘　　要：随着CPS在工业控制、智能交通、智能医疗等领域的广泛应用,安全性已成为目前CPS理论和应用研究的核心问题.提出了一种基于微分代数动态逻辑的CPS安全性验证方法,该方法首先把HybridUML模型转换成微分代数程序,然后使用微分代数动态逻辑对系统安全性进行规约,最后依据微分代数动态逻辑推理规则对CPS进行安全性验证.通过对飞机空中避撞系统的实例研究,表明该方法能够有效地验证避撞策略的正确性,从而保证避撞系统的安全性.With the wide use of cyber physical systems in industrial control, intelligent transportation system, intelligent medical and other areas, safety has been the core problem of the recent cyber physical systems theory and application research. In this paper, a safety verification method based on differential-algebraic dynamic logic is proposed. The method firstly transforms HybridUML model to differential-algebraic program, then realizes the specification of system safety using differential- algebraic program, and finally the cyber physical systems safety is verified according to differential- algebraic program reasoning rules. Through the case study of airplane collision avoidance system, it is shown that the method can verify the validity of the collision avoidance manoeuver effectively and guarantee the safety of airplane collision avoidance system.

关 键 词：信息物理融合系统 微分代数动态逻辑 HybridUML 微分代数程序 验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]