Automatic generation of formal models for diagnosability of DES

This paper aims at defining a model-driven approach for the diagnosability analysis of discrete event systems (DES). The proposed approach can be adopted during the design of modern control systems, in which many sensors and actuators are employed and the diagnosability of faults within a certain delay could be an issue. The proposal represents a first step towards an automatic model-driven process which derive formal models from a complete high-level specification of DESs. The specification activity of our approach relies on the Dynamic STate Machine (DSTM) formalism, a new language that extends state machines with dynamic instantiation, interrupts and asynchronous communication. The paper will describe how we can automatically derive Petri net and Promela models from the high-level DSTM specification. The former model can be used to apply diagnosability analysis approaches proposed in the DES community, while the latter can be used to apply model checking techniques. An application of the proposed model-driven approach is described by deriving both a PN and a Promela model for the well-known railway level crossing benchmark.