Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Derivation and Formal Verifica...

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

Yuliya Prokhorova, Linas Laibinis, Elena Troubitsyna, Kimmo Varpaaniemi, Timo Latvala, Derivation and Formal Verification of a Mode Logic for Layered Control Systems. In: Tran Dan Thu, Karl Leung (Eds.), Proceedings of the 18th Asia-Pacific Software Engineering Conference (APSEC 2011), 49–56, IEEE Conference Publishing Services (CPS), 2011.

Abstract:

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.

BibTeX entry:

@INPROCEEDINGS{iPrLaTrVaLa11a,
  title = {Derivation and Formal Verification of a Mode Logic for Layered Control Systems},
  booktitle = {Proceedings of the 18th Asia-Pacific Software Engineering Conference (APSEC 2011)},
  author = {Prokhorova, Yuliya and Laibinis, Linas and Troubitsyna, Elena and Varpaaniemi, Kimmo and Latvala, Timo},
  editor = {Thu, Tran Dan and Leung, Karl},
  publisher = {IEEE Conference Publishing Services (CPS)},
  pages = {49–56},
  year = {2011},
  keywords = {Event-B, formal specification, fault-tolerance, FMEA, mode logic, layered control systems},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication