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

Symbolic Model Checking for Discrete Real-time Linear Dynamic Logic

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

The appearance of errors in real-time systems is often dangerous or even fatal and using model checking to ensure the correctness of complex real-time systems is very effective.Aiming at the problem that traditional temporal logic can not express real-time properties and all regular properties in model detection,a Discrete Real-time Linear Dynamic Logic(RTLDL)with the ability to express discrete real-time properties and all regular property is proposed.Then,a labeling method which is similar to the program control flow labeling is defined to label the start and stop position for the RTLDL formula.Then,the temporal tester was constructed for the RTLDL formula based on the start-stop label relationship,and the Symbolic model checking algorithm based on the temporal tester for RTLDL is proposed.Finally,the proposed algorithm is implemented on the famous model checker NuXmv by a translation-based approach,and the experiment is compared with the currently only known LDL model checker MCMAS-LDLK on the guardrail control system.The experimental results show that the proposed algorithm is significantly efficient than MCMAS-LDLK for both LDL and RTLDL parts.