Object oriented approach for deriving feared scenarios in hybrid systems

This paper introduces a new method for modelling and analysis of the safety of systems that are hybrid in nature. It is based on a qualitative analysis of a Petri net model of the system with temporal abstraction of its continuous dynamics. The object-oriented concepts are used to provide modularity and handle system complexity; the global analysis problem is divided into a set of local problems. This method allows deriving feared scenarios by determining the sequences of actions and state changes leading to feared states in which the system fails. To avoid state space explosion Petri net reachability is translated into provability of linear logic sequent.