A Practical Method for the Reachability Analysis of Real-Time Systems Modelled as Timed Automata
Real-Time Systems (RTSs) interact with their environment 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).