基于DATL的信息物理融合系统安全性建模与验证  

Model and verification of safety of cyber-physical systems based on DATL

作　　者：周颖[1] 段鹏飞[1] 翟小祥[1] 李必信[1] Zhou Ying;Duan Pengfei;Zhai Xiaoxiang;Li Bixin(School of Computer Science and Engineering, Southeast University, Nanjing 211189, China)

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

出　　处：《东南大学学报（自然科学版）》2017年第1期12-17,共6页Journal of Southeast University：Natural Science Edition

基　　金：国家自然科学基金资助项目(61572008)

摘　　要：为解决微分时态动态逻辑(d TL)表达能力弱以及微分代数动态逻辑(DAL)缺少时序表达能力的问题,提出了一种结合d TL和DAL的微分代数动态时态逻辑(DATL).采用微分代数程序(DAP)作为操作模型,使DAL具有d TL的时序处理能力.定义了DATL操作模型的DAP和DATL语法,给出了DAP的迹语义和DATL语义,在继承d TL和DAL规则的基础上新增了6个规则.通过对飞机避撞系统安全性的规约和验证,检验了DATL的有效性.To solve the problem that the expression of the differential temporal dynamic logic(dTL)is weak and the temporality expression of the differential-algebraic dynamic logic(DAL)is lack,a differential-algebraic temporal dynamic logic(DATL)based on the dTL and the DAL was proposed.The differential-algebraic program(DAP)was used as the operating model and the ability of handling temporality of the dTL was introduced into the DAL.The syntax of both the DAP and the DATL formulas were defined.Both the trace semantics of DAP and the semantics of the DATL formulas were presented.The six new rules were added based on the existing rules of dTL and DAL.Finally,the safety of the aircraft collision avoidance system were modeled and verified,proving the effectiveness of the DATL.

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

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