Using SWN nets to specify and analyze FT mechanisms adopted in electric plant automation

The increasing complexity of automation systems, which combine high functional, real-time and fault-tolerant requirements, demands for techniques and tools to support design choices and validation phases. In this paper we investigate the possibility of using a class of high-level stochastic Petri nets known as stochastic well-formed nets (SWN) as a framework for specifying and deriving quantitative properties of FT mechanisms used in (electric) plant automation. A temporal redundancy technique adopted in several plants is taken as a case-study.