Performance-based characterization of fault tolerant embedded electric applications by means of stochastic hlpn models

In embedded automation systems, functional, performance and fault-tolerant (FT) requirements are strongly related. The use of formal models since the early design phases of such systems is by now considered not only as a promising opportunity, but as a real need. From this point of view a challenging issue is the possibility of integrating/combining the different modeling approaches that are usually adopted in the specification and val idation/evaluation phases. In this paper we present a selection of outcomes of a modeling activity started some years ago, that aims at experiencing a class of High-Level Stochastic Petri Nets (SWNs) as unifying specification/analysis framework in the field of embedded FT electric applications. We here focus on the speci fication and the performance-based characterization of the the stable memory mechanism, the blueprint of a FT architecture still employed in several plants of the Italian electric power distribution network. In particular we show that quantitative results can be also used to infer interesting functional properties of the mechanism