Derivation and Formal Verification of a Mode Logic for Layered Control Systems

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

Full description

Saved in:
Bibliographic Details
Main Authors: Prokhorova, Y., Laibinis, L., Troubitsyna, E., Varpaaniemi, K., Latvala, T.
Format: Conference Proceeding
Language:English
Subjects:
Attitude control
Control systems
Event-B
Fault tolerance
Fault tolerant systems
FMEA
formal specification
Global Positioning System
Instruments
layered control systems
mode logic
Satellites
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1530-1362
2640-0715
DOI:10.1109/APSEC.2011.38