Symbolic Model Checking Real-time Temporal Logic RTCTL * With BDDs And The Witness Generation

Model checking is a more effective method of verifying the correctness and reliability of the system. There are some critical applications where predictable predictable response times are essential for correctness. Due to the nature of such applications, errors in these real-time systems can be extremely dangerous,even fatal. Most of the real-time system has its own effective activity time, so we only need to test its performance and parameters of a certain period of time. So the key problem what we want to solve is Real-Time Temporal Logic RTCTL*,which expands the scope of logic description,its expressive power is stronger. So the study of RTCTL* has important influence and significance.The main work of this thesis can be summarized as follows:1.A Just Discrete System( JDS) was constructed as our computational model, which is a finite-state transition system with weak fairness constraints,and we gave a method of the synchronous parallel composition of JDS ’s;2.We proposed the syntax of RTCTL* and the semantics of RTCTL*.To facilitate expressing various formulas, we added some additional operators to RTCTL* by some equations;3.By mapping RTCTL* formulas to state formulas,the problem of model checking RTCTL* becomes the problem of CTL.And then we provided the algorithms of symbolic model checking Real-time Temporal Logic RTCTL* with BDDs.This method proved to be sound and complete at last;4.We demonstrated counterexample and witness are two symmetrical concepts.And we presented the approach of witness generation in this paper.