Based On Timed Automata, Real-time System Specification Validation Study

Real-time systems demand the correctness of time as well as logic, which demand rigorous analyses and verification during the design stage. Timed automata is one of the most used methods for specifying and verifying real-time systems.Verification of real-time systems includes checking safety properties and liveness properties. Liveness properties can be guaranteed by invariant and clock constraints and its verification is easy. So we won't consider it too much in this paper. The checking of safety properties is based on the analysis and state space checking. The major weakness of the state space exploration is that the size of the state space grows exponentially with the number of processes, which creates the state space explosion problem. So we must construct the finite representation of the reachable states.In this paper, we research region automata, zone automata and the method of state space minimization developed by Inhye Kang. Further, we develop time segment transition system and a method of state space minimization. The method use location and the possible time distance staying in this location to denote the state. We reduce it using transition analysis and removing off invalid transition. Then, we use transition bisimulation to minimize the transition system. In the paper, we analyses the feasibility of the method, and show its advantage and disadvantage by comparing it with others. We also construct the minimal process of train-gate control systems.Considering the application of specification and verification, we research two kinds of real time systems-turnout auto control systems and auto sizer systems. We give the timed automata models of them by analyses and specification, and check them by UPPAAL, which demonstrate the safety, efficiency and controllability of the systems.