In: Proc. 9th IFAC Symp. on Information Control in Manufacturing (INCOM'98), 24-26 June 1998, Nancy-Metz, France, Vol. 1, pages 223-228. 1998.
Abstract: Synchronous data flow languages are designed for programming reactive systems and especially those which must abide safety critical requirements. Based on simple and clean mathematical principles, one of the salient benefits of the synchronous approach is its ability to support formal design and formal verification. However, to formally verify that a specification complies with some critical properties, it is necessary to define some assumptions about the behavior of the environment. Probabilistic safety assessment deals with potential failure modes of the system environment. Generalized stochastic Petri nets are used to assess probabilities of failure modes. The combination of both approaches - formal and probabilistic -- allows to increase the confidence in the system. This paper presents the experience of Schneider Electric gained in the use of such methods.
Keywords: formal methods, probabilistic methods, safety critical systems, stochastic Petri nets, synchronous languages.