Formal Modeling And Verification Of Real-time Systems Based On Time Automation

Real-time system is a kind of systems with time constraint. The action is connected with some time constraint. Correctness and security are important to these systems, so analysis and validation are needed, The validation of real-time systems not only needs the logic is correct, but also the time is correct. The time automata is the most to be put into use building the formalize model implement of real time system.Based on timed automata developed by R.Alur, theories of specification and verification of real-time systems and their applications are described in this paper.By giving timed automata of formalize definition in this paper, we have studied real-time systems modeling method basing on time automata, and have given timed antomata model optimization out method. We carried out analysis on two real-time systems finally, and maked use of the timed automata to build a model to them .Verification of real-time systems includes checking safety properties and liveness properties. The checking of safety properties is based on the analysis and state space checking.But the bottleneck is the state space explosion problem when constructing systems by model checking method. Then it is in great need of the formal technique of automatic verification to solve these problems.To solve the problem of state-space explosion which appeared in the area automata organization builds process, We have quoted the elicitation method verifying method.This paper has been studied mainly owing to history and the minimized method changing imitating mutually. The state space explosion problem can be facilitated greatly by minization.UPPAAL is a kind of model verification tool, which takes the timed automata as its behavioral model and plays a very important role in the specification and verification of real-time systems and communication protocols. To resolve the problem of state-space explosion, UPPAAL uses constraint solving techniques and forward verification techniques to avoid building the state space that are not reachable.Finally, making use of UPPAAL to carry out the function verification on the systematic two timed automata model of real-time systems already building, we have testified their correctness and security.