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

TL;DR

This paper reviews recent advances in using Event-B for formal dependability engineering, including safety analysis, fault tolerance, and probabilistic evaluation within the EU Deploy project.

Contribution

It presents new formal approaches for dependability reasoning in Event-B, integrating safety, fault tolerance, and probabilistic analysis into system development.

Findings

Successful integration of safety analysis into Event-B models

Development of fault-tolerant system modeling techniques

Advances in probabilistic dependability evaluation methods

Abstract

Event-B has been actively used within the EU Deploy project to model dependable systems from various application domains. As a result, we have created a number of formal approaches to explicitly reason about dependability in the refinement process. In this paper we overview the work on formal engineering of dependable systems carried out in the Deploy project. We outline our approaches to integrating safety analysis into the development process, modelling fault tolerant systems and probabilistic dependability evaluation. We discuss achievements and challenges in development of dependable systems within the Event-B framework.