A Practical Method for the Reachability Analysis of Real-Time Systems Modelled as Timed Automata

Abstract—Real-time systems (RTSs) interact with their en-vironment under time constraints. Such constraints are so critical because any deviation from the specified deadlines might have severe consequences on both the human lives and the environment. To develop reliable RTSs, formal methods should be used along the development life cycle. Verification is one of these formal methods, which aims at ensuring that the system is correct before its deployment. This paper presents a new verification method for the reachability analysis of real-time systems modelled as timed automata (TA) [1]. The paper basically addresses two main issues: are all the transitions of the system executable? Are all the locations reachable from the initial location of the system? In order to answer these questions, our method uses a metric that gives the minimum delay between any state and all the transitions leaving that state