Integrating safety analysis into formal specification of dependable systems

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.