Clocks Manipulation Applying To The Formal Verificationof Timed System

The real-time system is a way to specify that the system completes the functionswithin adetermined time, and make a timely response to external and internal random events insynchronous or asynchronous time. Currently, the real-time system has been involved in the vastmajority fields, for example the application of embedded systems in our daily life and militaryfields. Since embedded systems are not closed system, theyare often in a larger systemand play amajor impact on the entire system by controlling system operation. Almost all of the safety-criticalsystems and most embedded systems are real-time systems. Therefore, it ismeaningfulandimportant toensure the correctness of real-time system design.In order to ensure the correctness of the system design, we are needed to checkwhether thesystem model satisfies certain property or not. Due to the introduction of thereal-valued time,formal verification fortime systems is more challenging. Because clock value is continuous andmonotonically increasing, the real-time system state space is infinite and the traditional untimedsystem verification methodsare not suitable for the real-time system verification. Simulationgraphof the real-time system is a zone-based transition system. According to region equivalence,the infinite state space is equivalentlydivided into a finitestate space. In this thesis, we use regionconstruction technology to solve thestate space explosion problem, and propose a verificationframework PVofTA which automatically check the required properties of the real-time systembased on the simulation graph technology.Thespecificworkis as following:Firstly, under the preliminary work of ourresearch group, FormalVerification ofTimeAutomatonframework which is short for FVofTA and the based-on predicate abstractionverification template oftimed automata ExTA,we further analysis the syntax oftimed automata andthesemantics ofits transition system and associated properties, specially the clock constraints andzones which are present as Difference Bound Matric and tightened to canonical form, to make itmore conducive to application and automation in practice.Secondly,on the basis of research work on the TBA’s emptiness checkingand the simulationgraph technology,we propose areal-time system verification framework to automaticallycheck thesatisfaction of its properties. By the definition of product automata, we calculate the productautomaton of the whole real-time system by synchronizing the subsystems and at the same time,withforward calculation operator Post, we calculate the simulation graph of the product automatonby starting from the initial node. The liveness property and reachability property are twofundamental properties for real-time system. Therefore, according to some researches, the propertychecking of the real-time system can be converted into some state’s reachability checking or thesimulation graph’s emptiness checkingfor lasso paths. By the way,we also give the details of theproduct automata and simulation graph calculation process through specific examples.Finally, given the verification framework, we implement the templates with use of theadvanced language technology and check them on a specific example, the classical real-timesystem"Railway Crossing System", to further verify the feasibility and practicality of theframework.In summary, to resolve the system state space explosion problem, this paperanalyze and research on the region construction and simulation graph. On the basis of above work, we proposea verification framework for the property satisfaction checking of real-time system and then putthe framework in practice,check them on specific examples. All these work is aimed to automatizethe formal verification of real-time systems and improve the efficiency.