Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements
---
paper_title: Resilience for the Scalability of Dependability

paper_content:

The current state-of-knowledge and state-of-the-art reasonably enable the construction and operation of critical systems, be they safety-critical or availability-critical. The situation drastically worsens when considering large, networked, evolving, systems either fixed or mobile, with demanding requirements driven by their domain of application. There is statistical evidence that these emerging systems suffer from a significant drop in dependability and security in comparison with the former systems. The cost of failures in service is growing rapidly, as a consequence of the degree of dependence placed on computing systems, up to several million euros per hour of downtime for some businesses
---
paper_title: Resilience for the Scalability of Dependability

paper_content:

The current state-of-knowledge and state-of-the-art reasonably enable the construction and operation of critical systems, be they safety-critical or availability-critical. The situation drastically worsens when considering large, networked, evolving, systems either fixed or mobile, with demanding requirements driven by their domain of application. There is statistical evidence that these emerging systems suffer from a significant drop in dependability and security in comparison with the former systems. The cost of failures in service is growing rapidly, as a consequence of the degree of dependence placed on computing systems, up to several million euros per hour of downtime for some businesses
---
paper_title: Developing mode-rich satellite software by refinement in event B

paper_content:

To ensure dependability of on-board satellite systems, the designers should, in particular, guarantee correct implementation of the mode transition scheme, i.e., ensure that the states of the system components are consistent with the global system mode. However, there is still a lack of scalable approaches to formal verification of correctness of complex mode transitions. In this paper we present a formal development of an Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. AOCS is a complex mode-rich system, which has an intricate mode-transition scheme. We show that refinement in Event B provides the engineers with a scalable formal technique that enables both development of mode-rich systems and proof-based verification of their mode consistency.
---
paper_title: Verifying mode consistency for on-board satellite software

paper_content:

Space satellites are examples of complex embedded systems. Dynamic behaviour of such systems is typically described in terms of operational modes that correspond to the different stages of a mission and states of the components. Components are susceptible to various faults that complicate the mode transition scheme. Yet the success of a mission depends on the correct implementation of mode changes. In this paper we propose a formal approach that ensures consistency of mode changes while developing a system architecture by refinement. The approach relies on recursive application of modelling and refinement patterns that enforce correctness while implementing the mode transition scheme. The proposed approach is exemplified by the development of an Attitude and Orbit Control System undertaken within the ICT DEPLOY project.
---
paper_title: Derivation and Formal Verification of a Mode Logic for Layered Control Systems

paper_content:

Modes are widely used to structure the behaviour of control systems. For many such systems, derivation and verification of a mode logic is challenging due to a large number of modes and complex mode transitions. In this paper we propose an approach to deriving, formalising and verifying consistency of a mode logic for fault tolerant control systems. We demonstrate how to use Failure Modes and Effects Analysis (FMEA) to systematically derive the fault tolerance part of the mode logic. To tackle the problem of mode consistency, we propose a formalisation of the mode logic and mode consistency conditions for layered systems with reconfigurable components. We use our formalisation to develop and verify a mode-rich system by refinement in Event-B.
---
paper_title: Developing Mode-Rich Satellite Software by Refinement in Event B

paper_content:

One of the guarantees that the designers of on-board satellite systems need to provide, so as to ensure their dependability, is that the mode transition scheme is implemented correctly, i.e. that the states of system components are consistent with the global system mode. There is still, however, a lack of scalable approaches to developing and verifying systems with complex mode transitions. This paper presents an approach to the formal development of mode-rich systems by refinement in Event-B. We formalise the concepts of modes and mode transitions as well as deriving specification and refinement patterns which support correct-by-construction system development. The proposed approach is validated by a formal development of the Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. The experience gained in the course of developing such a complex industrial system as AOCS, shows that Event-B refinement provides the engineers with a scalable formal technique. Moreover, the case study has demonstrated that Event-B can facilitate formal development of mode-rich systems and, in particular, proof-based verification of their mode consistency.
---
paper_title: A case study in formal development of a fault tolerant multi-robotic system

paper_content:

Multi-robotic systems are typical examples of complex multi-agent systems. The robots --- autonomic agents --- cooperate with each other in order to achieve the system goals. While designing multi-robotic systems, we should ensure that these goals remain achievable despite robot failures, i.e., guarantee system fault tolerance. However, designing the fault tolerance mechanisms for multi-agent systems is a notoriously difficult task. In this paper we describe a case study in formal development of a complex fault tolerant multi-robotic system. The system design relies on cooperative error recovery and dynamic reconfiguration. We demonstrate how to specify and verify essential properties of a fault tolerant multi-robotic system in Event-B and derive a detailed formal system specification by refinement. The main objective of the presented case study is to investigate suitability of a refinement approach for specifying a complex multi-agent system with co-operative error recovery.
---
paper_title: Formal development and assessment of a reconfigurable on-board satellite system

paper_content:

Ensuring fault tolerance of satellite systems is critical for achieving goals of the space mission. Since the use of redundancy is restricted by the size and the weight of the on-board equipments, the designers need to rely on dynamic reconfiguration in case of failures of some components. In this paper we propose a formal approach to development of dynamically reconfigurable systems in Event-B. Our approach allows us to build the system that can discover possible reconfiguration strategy and continue to provide its services despite failures of its vital components. We integrate probabilistic verification to evaluate reconfiguration alternatives. Our approach is illustrated by a case study from aerospace domain.
---
paper_title: Formal Development of Critical Multi-agent Systems: A Refinement Approach

paper_content:

Multi-agent systems (MAS) are increasingly used in critical applications. To ensure dependability of MAS, we need powerful development techniques that would allow us to master complexity inherent to MAS and formally verify correctness and safety of collaborative agent activities. In this paper we present a development of hospital MAS by refinement in Event-B. We demonstrate that Event-B allows the developers to rigorously specify complex agent interactions and verify their correctness and safety.
---
paper_title: Formal goal-oriented development of resilient MAS in event-b

paper_content:

Goal-Oriented Development facilitates structuring complex requirements. To ensure resilience the designers should guarantee that the system achieves its goals despite changes, e.g., caused by failures of system components. In this paper we propose a formal goal-oriented approach to development of resilient MAS. We formalize the notion of goal and goal achievement in Event-B and propose the specification and refinement patterns that allow us to guarantee that the targeted goals are reached despite agent failures. We illustrate our approach by a case study --- development of an autonomous multi-robotic system.
---
paper_title: Patterns for Representing FMEA in Formal Specification of Control Systems

paper_content:

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.
---
paper_title: Formal modelling and verification of service-oriented systems in probabilistic event-b

paper_content:

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.
---
paper_title: Linking modelling in event-b with safety cases

paper_content:

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.
---
paper_title: Formal modelling and verification of service-oriented systems in probabilistic event-b

paper_content:

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.
---

Title: Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements

Section 1: Introduction
Description 1: Provide an overview of the increasing importance of dependability in computer-based systems, the inadequacies in current development processes, and how the FP7 EU Deploy project addresses these issues using Event-B.

Section 2: Event-B
Description 2: Explain the Event-B development approach, including its methods of managing system complexity through abstract modeling, decomposition, iterative development, and the roles of refinement and the Rodin platform.

Section 3: Dependability in System Development
Description 3: Discuss the broad notion of dependability, focusing on safety, reliability, and availability, and describe how Event-B contributes to fault prevention, fault tolerance, fault removal, and fault forecasting in system development.

Section 4: Formal development of fault tolerant mode-rich systems
Description 4: Describe the approach to formal development of fault-tolerant, mode-rich systems, emphasizing the layer-by-layer development, verification of mode consistency, and methods such as FMEA for implementing fault tolerance.

Section 5: Goal-oriented refinement of reconfigurable systems
Description 5: Explore the approach for developing goal-oriented and dynamically reconfigurable systems, including modeling patterns for agent roles, mechanisms for dynamic reconfiguration, and integration of probabilistic analysis for assessing dependability.

Section 6: Integrating Safety Analysis into Formal Development
Description 6: Outline the integration of safety analysis methods like FMEA into formal development using Event-B, discussing patterns for formal requirements and automating the formal development process to verify safety invariants and generate evidence for safety cases.

Section 7: Quantitative Assessment of Dependability
Description 7: Explain how quantitative constraints are integrated into Event-B refinement to ensure that models improve or preserve dependability attributes, and describe case studies validating these approaches, including fault-tolerant and safety-critical systems.

Section 8: Discussion
Description 8: Summarize the contributions of the FP7 EU Deploy project, highlighting the development of modeling patterns, integration of safety and reliability analysis, and insights gained from industrial case studies. Discuss future directions to enhance scalability, tool support, and heterogeneous modeling techniques in Event-B.