|
|||||
|
|
| 基于DATL的信息物理融合系统安全性建模与验证 | |
| 摘 要： | 为解决微分时态动态逻辑(d TL)表达能力弱以及微分代数动态逻辑(DAL)缺少时序表达能力的问题,提出了一种结合d TL和DAL的微分代数动态时态逻辑(DATL).采用微分代数程序(DAP)作为操作模型,使DAL具有d TL的时序处理能力.定义了DATL操作模型的DAP和DATL语法,给出了DAP的迹语义和DATL语义,在继承d TL和DAL规则的基础上新增了6个规则.通过对飞机避撞系统安全性的规约和验证,检验了DATL的有效性. |
| 本文献已被 CNKI 等数据库收录！ | |