Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Integrating Safety Analysis into Formal Development <s> Failure Modes and Effects analysis (FMEA) is a widely used technique for inductive safety analysis. FMEA provides engineers with valuable information about failure modes of system components as well as procedures for error detection and recovery. In this paper we propose an approach that facilitates representation of FMEA results in formal Event-B specifications of control systems. We define a umber of patterns for representing requirements derived from FMEA in formal system model specified in Event-B. The patterns help the developers to trace the requirements from safety analysis to formal specification. Moreover, they allow them to increase automation of formal system development by refinement. Our approach is illustrated by an example - a sluice control system. <s> BIB001 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Integrating Safety Analysis into Formal Development <s> Safety cases are adopted in the certification process of many safety-critical systems. They justify why a system is safe and whether the design adequately incorporates safety requirements defined in a system requirement specification. The use of formal methods facilitates modelling and verification of safety-critical systems. In our work, we aim at establishing a link between formal modelling in Event-B and constructing a safety case. We propose an approach to incorporating safety requirements in a formal specification in such a way that it allows the developers to derive a safety case sufficient to demonstrate safety. We present a small case study illustrating the proposed approach. <s> BIB002 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Integrating Safety Analysis into Formal Development <s> Modelling and refinement in Event-B provides a scalable support for systematic development of complex service-oriented systems. This is achieved by a gradual transformation of an abstract service specification into its detailed architecture. In this paper we aim at integrating quantitative assessment of essential quality of service attributes into the formal modelling process. We propose an approach to creating and verifying a dynamic service architecture in Event-B. Such an architecture can be augmented with stochastic information and transformed into the corresponding continuous-time Markov chain representation. By relying on probabilistic model-checking techniques, we allow for quantitative evaluation of quality of service at early development stages. <s> BIB003
In BIB001 , we have demonstrated how to combine formal modelling and refinement with Failure Modes and Effects Analysis (FMEA). We have defined a set of patterns formalising the requirements derived from FMEA as well as automated their integration into the formal specification. The proposed approach facilitates formal development and improves traceability of safety requirements. The approach proposed in this paper allows us to automate the formal development process via two main steps: choice of suitable patterns that generically define FMEA result, and instantiation of chosen patterns with model-specific information. Our approach allows the developers to verify (by proofs) that safety invariants are preserved in spite of identified component failure modes. Hence we believe that it provides a useful support for formal development and improves traceability of safety requirements. The use of an evidence generated from formal analysis is still an open issue in the system certification process. Sometimes the formal proofs deemed to be too complex and cause doubts regarding their trustworthiness as the evidence in safety cases of safety-critical systems. Another open issue related to the formal modelling process is whether the obtained formal model adequately represents safety requirements described in a system specification. In our work BIB002 we proposed an approach to linking formal modelling in Event-B with safety cases. We give the classification of safety requirements and define how each class can be represented in a formal specification. The approach allows the developers to obtain a consistent system specification that facilitate deriving a sufficient safety case. The systems, whose components are susceptible to various kinds of faults, never are "absolutely" safe, i.e., certain combinations of failures may lead to an occurrence of a hazard -a potentially dangerous situation breaching safety requirements. To demonstrate that the probability of a hazard occurrence is acceptably low, in  we have presented a formal approach to integrating quantitative safety analysis into formal system development by refinement in Event-B. Essentially, our approach can be seen as a process of extracting a fault treea logical representation of a hazardous situation in terms of the primitives used at different abstraction layers. Eventually, we arrive at the representation of a hazard in terms of the failures of basic system components, which allows us to calculate probability of a hazard occurrence. The proposed approach is based on a probabilistic extension of Event-B BIB003 . It enables development of systems that are not only correct but also safe by construction.