Model Checking For Discrete Real-Time Linear Dynamic Logic

Real-time systems are widely used in the processing of some major and urgent events,such as intelligent robots,aerospace systems and railway dispatching systems.Once an error occurs in a real-time system,the consequences are often very dangerous or even catastrophic.This requires that the real-time system must have high accuracy to ensure the specific response time of each module in the system.Model checking is of great help to detect the correctness of real-time system.However,the existing real-time extension of the temporal logic is mainly based on the traditional temporal logic.It lacks the ability to express regular attributes and cannot describe some behaviors of complex real-time systems.Therefore,we add time interval constraints on the Linear Dynamic Logic(LDL),and propose a discrete Real-Time Linear Dynamic Logic(RTLDL)with the ability to express discrete real-time properties and all regular attributes,so it can easily describe the behavior of some complex real-time systems.We propose an RTLDL symbolic model checking algorithm based on the temporal tester.Then we implement our algorithm by translating the constructed tester into specific smv program modules,and running the tester program on the well-known model checking tool nu Xmv.The main work of thesis is as follows:(1)A new real-time temporal logic RTLDL is proposed,which is an extension of the real-time nature of LDL,so that LDL can express and analyze the real-time behavior of the system;(2)We construct temporal testers for the basic temporal operators based on the idea of program control flow labeling to solve the model checking problem of LDL.Based on this,a tester with a bounded temporal formula is further constructed,and an RTLDL symbolic model checking algorithm based on the tester is proposed;(3)We use the translation method to verify the proposed algorithm on model checking tool nu Xmv.The experimental results show that,when verifying the RTLDL formula,our method is significantly better than the model checking tool MCMAS-LDLK,which is the only model checking tool that implements LDL model checking,especially for RTLDL formulas that do not contain bounded test formula nested in Kleene Star,our algorithm is exponentially superior to MCMAS-LDLK.