-
题名离散实时线性动态逻辑的符号化模型检测
- 1
-
-
作者
骆翔宇
许杭娜
曾昊晟
陈祖希
杨帆
-
机构
华侨大学计算机科学与技术学院
华侨大学机电及自动化学院
-
出处
《计算机科学》
CSCD
北大核心
2020年第9期204-212,共9页
-
基金
国家自然科学基金重点项目(61733006)
国家自然科学基金面上项目(61170028)
+1 种基金
福建省自然科学基金面上项目(2015J01255)
福建省高等学校新世纪优秀人才支持计划项目(2013FJ-NCET-ZR03)。
-
文摘
实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较。实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。
-
关键词
符号化模型检测
时态测试器
实时线性动态逻辑
离散实时系统
-
Keywords
Symbolic model checking
Temporal tester
Real-time linear dynamic logic
Discrete real-time systems
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-