Title: Deriving a mode logic using failure modes and effects analysis

Authors: Yuliya Prokhorova; Linas Laibinis; Elena Troubitsyna; Kimmo Varpaaniemi; Timo Latvala

Addresses: TUCS – Turku Centre for Computer Science, Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520 Turku, Finland ' TUCS – Turku Centre for Computer Science, Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520 Turku, Finland ' TUCS – Turku Centre for Computer Science, Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520 Turku, Finland ' Space Systems Finland, Kappelitie 6 B, 02200 Espoo, Finland ' Space Systems Finland, Kappelitie 6 B, 02200 Espoo, Finland

Abstract: Modes are widely used to structure the behaviour of control systems. However, derivation and verification of a mode logic for complex systems is challenging due to a large number of modes and intricate 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 propose to use failure modes and effects analysis (FMEA) to systematically derive the fault tolerance part of the mode logic. We formalise the mode logic and define mode consistency properties for layered systems with reconfigurable components. We use our formalisation to develop and verify a mode-rich system by refinement in Event-B.

Keywords: Event-B; formal specification; fault tolerance; failure mode and effects analysis; FMEA; layered control systems; mode logic; reconfigurable components.

DOI: 10.1504/IJCCBS.2012.053206

International Journal of Critical Computer-Based Systems, 2012 Vol.3 No.4, pp.305 - 328

Published online: 16 Aug 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article