This paper presents and validates a novel approach to a formal specification of software for dependable systems. The approach incorporates results of statecharts and Failure Mode and Effect Analysis (FMEA) in the development of formal specifications of fail-safe systems. We use the action system formalism as our specification framework. Within the framework we define a general model of a safety-critical fail-safe system. Statecharts facilitate construction of a formal specification by structuring informal functional requirements and formalizing safety requirements resulted from FMEA. The approach is validated by a case study — a derivation of formal specification of a conveyor system.
Index Terms:
statecharts, failure mode and effect analysis, actions systems, formal specification
Citation:
Elena Troubitsyna, "Integrating Safety Analysis into Formal Specification of Dependable Systems," ipdps, pp.215b, International Parallel and Distributed Processing Symposium (IPDPS'03), 2003