ORIS: A TOOL FOR STATE-SPACE ANALYSIS OF REAL-TIME PREEMPTIVE SYSTEMS

Abstract - Formal methods based on state-space enumeration, such as Timed Automata and Time Petri Nets (TPN), have been proposed for designing and validating reactive real-time systems. The great expressiveness of these methods is coun- terbalanced by the increased complexity of the analysis, which may grow exponentially. Furthermore, the enumer- ated state-space needs to be inspected to identify critical behaviors with respect to sequencing and timing require- ments. This naturally leads to the implementation of tools supporting the different stages of the development process. In this paper we present Oris, an environment for build- ing, simulating, analyzing and validating complex real time systems specified in terms of an extended TPN formalism, named Preemptive Time Petri Nets. Oris includes not only the state-space enumeration engine, but also a number of modules which ease user interaction, and make it usable also by a designer with no specific experience in formal modelling.