Development of Safety-Critical Control Systems in Event-B Using FMEA

Development of Safety-Critical Control Systems in Event-B Using FMEA

Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis, Vyacheslav S. Kharchenko
Copyright: © 2012 |Pages: 17
DOI: 10.4018/978-1-60960-747-0.ch005
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

Application of formal methods, in particular Event-B, helps us to verify the correctness of controlling software. However, to guarantee the dependability of software-intensive control systems, we also need to ensure that safety and fault tolerance requirements are adequately represented in a system specification. In this chapter we demonstrate how to integrate the results of safety analysis, in particular failure mode and effect analysis (FMEA), into formal system development in Event-B. The proposed methodology is exemplified by a case study.
Chapter Preview
Top

Integration of the safety analysis techniques with formal system modelling has attracted a significant research attention over the last few years. There are a number of approaches that aim at direct integration of the safety analysis techniques into formal system development. For instance, the work of Ortmeier et al. (Ortmeier, Guedemann, & Reif, 2007) focuses on using statecharts to formally represent the system behaviour. It aims at combining the results of FMEA and FTA to model the system behaviour and reason about component failures as well as overall system safety. Moreover, the approach specifically addresses formal modelling of the system failure modes. In our approach we define general guidelines for integrating results of FMEA into a formal Event-B specification and the Event-B refinement process. The available automatic tool support for the top-down Event-B modelling ensures better scalability of our approach.

Complete Chapter List

Search this Book:
Reset