Study And Implementation Of Reachability Algorithm On Updatable Timed Automata

Real-time systems are widely used in the areas of aerospace, military and nuclearindustry, but its complexity makes it really difficult to guarantee the security andreliability. Formal verification theory which is based on the calculation model plays asignificant role in real-time systems to guarantee its security and reliability. Anupdatable timed automaton is a valid model which could give an efficient descriptionof the behavior of real-time systems. This model for real-time systems could be usedto ensure high reliability in analysis, design and verification. However, it’s still intheoretical development. The problem the reachability is one of the key issues of thecalculation model.An updatable timed automaton extends timed automata with updates. There aremany similarities and of cause differences. In this paper, problems are solved causedby such extension which makes the reachability algorithm possible in updatable timedautomata, also some implementation issues are solved.First, this paper gives the FRA algorithm in updatable timed automata which canensure the result in the case of diagonal-free constraints. Secondly, in the case of thegeneral constraints, we give the Select_guard algorithm which can filter the diagonalconstraint that can affect the reachability result. Also the updatable timed automatarefinement algorithm is provided to convert it to a timed automaton without theselected diagonal constraints. With such two-step, the erroneous judgment in the caseof general constraints is solved correctly. Then, the overall process andimplementation of the reachability algorithm in updatable timed automata is given.Finally, the experiment ensures the correctness of the algorithm and efficiency whichlaid the foundation for the development of the updatable time automata.