Reliability analysis of discrete event dynamic systems with Petri nets
Abstract
The purpose of this paper is to illustrate a method for addressing dynamic reliability of embedded systems using the Petri net model. The approach is based on the search of feared scenarios (which might lead the system to a critical situation) by proving some linear logic sequents that correspond to the ¯ring of a list of transitions of a Petri net. To avoid state space explosion, Petri net reachability is translated into provability of linear logic sequents. The method produces a number of scenarios, which may be redundant. To give relevant information to designers the scenarios must be minimal which means that only necessary events are included in a scenario. The concept of minimality of a scenario is de¯ned and introduced on the ESA-PetriNet tool that we have developed to implement the algorithm for the search of feared scenarios.