离散实时线性动态逻辑的符号化模型检测

摘要：

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的.针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较.实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MC-MAS-LDLK.

关键词：符号化模型检测、时态测试器、实时线性动态逻辑、离散实时系统

所属期刊栏目：47

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金重点项目;国家自然科学基金面上项目;福建省自然科学基金面上项目;福建省高等学校新世纪优秀人才支持计划项目

在线出版日期：2020-09-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：204-212