东南大学学报（自然科学版）2017，Vol.47Issue(1)：12-17,6.DOI:10.3969/j.issn.1001-0505.2017.01.003
基于DATL的信息物理融合系统安全性建模与验证
Model and verification of safety of cyber-physical systems based on DATL
摘要
Abstract
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 pro-posed.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 for-mulas 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.关键词
信息物理融合系统/属性验证/微分时序动态逻辑/微分代数动态逻辑/微分代数时序动态逻辑Key words
cyber-physical systems/property verification/differential temporal dynamic logic/dif-ferential-algebraic dynamic logic/differential-algebraic temporal dynamic logic分类
信息技术与安全科学引用本文复制引用
周颖,段鹏飞,翟小祥,李必信..基于DATL的信息物理融合系统安全性建模与验证[J].东南大学学报（自然科学版）,2017,47(1):12-17,6.基金项目
国家自然科学基金资助项目（61572008）． （）
