高级检索
    陈乔乔 李必信 吉顺慧. 一种基于微分代数动态逻辑的CPS建模与验证方法[J]. 计算机研究与发展, 2013, 50(4): 700-710.
    引用本文: 陈乔乔 李必信 吉顺慧. 一种基于微分代数动态逻辑的CPS建模与验证方法[J]. 计算机研究与发展, 2013, 50(4): 700-710.
    Chen Qiaoqiao, Li Bixin, and Ji Shunhui. A Modeling and Verification Method of CPS Based on Differential-Algebraic Dynamic Logic[J]. Journal of Computer Research and Development, 2013, 50(4): 700-710.
    Citation: Chen Qiaoqiao, Li Bixin, and Ji Shunhui. A Modeling and Verification Method of CPS Based on Differential-Algebraic Dynamic Logic[J]. Journal of Computer Research and Development, 2013, 50(4): 700-710.

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

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

    • 摘要: 随着CPS在工业控制、智能交通、智能医疗等领域的广泛应用,安全性已成为目前CPS理论和应用研究的核心问题.提出了一种基于微分代数动态逻辑的CPS安全性验证方法,该方法首先把HybridUML模型转换成微分代数程序, 然后使用微分代数动态逻辑对系统安全性进行规约,最后依据微分代数动态逻辑推理规则对CPS进行安全性验证.通过对飞机空中避撞系统的实例研究,表明该方法能够有效地验证避撞策略的正确性,从而保证避撞系统的安全性.

       

      Abstract: 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.

       

    /

    返回文章
    返回