A Non-Temporized Approach for Temporized Analysis

Real-time critical systems require extensive analysis. The potentially large damages caused by failures of real-time critical systems justify the use of expensive verification techniques, such as timed reachability analysis. Unfortunately the costs of timed reachability analysis inhibits its systematic application at the early stages of development, when long verification sessions could slow down the development process. Moreover, the large reachability space built for proving temporal properties reduces the size of specification for which timed reachability analysis can be applied. In this paper we show how reachability analysis of the non temporized underlying petri net can reduce the size of timed reachability analysis. In this way, timed reachability analysis can be used for analyzing industrial-size safety critical systems, paying an acceptable overhea