creators_name: Prokhorova, Yuliya
creators_name: Laibinis, Linas
creators_name: Troubitsyna, Elena
creators_name: Varpaaniemi, Kimmo
creators_name: Latvala, Timo
creators_id: Yuliya.Prokhorova@abo.fi
creators_id: Linas.Laibinis@abo.fi
creators_id: Elena.Troubitsyna@abo.fi
type: conference_item
datestamp: 2012-06-29 07:54:19
lastmod: 2012-06-29 07:54:19
metadata_visibility: show
title: Derivation and Formal Verification of a Mode Logic for Layered Control Systems
ispublished: pub
subjects: Event-Bsemantics
subjects: Refinement
subjects: deploy_industrial_space
subjects: deploy_method_proof
subjects: deploy_method_resil
subjects: examples
full_text_status: none
pres_type: paper
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.
date: 2011
date_type: published
pagerange: 49-56
event_title: The 18th Asia-Pacific Software Engineering Conference (APSEC 2011)
event_location: Ho Chi Minh, Vietnam
event_type: conference
refereed: TRUE
citation:   Prokhorova, Yuliya and Laibinis, Linas and Troubitsyna, Elena and Varpaaniemi, Kimmo and Latvala, Timo  (2011) Derivation and Formal Verification of a Mode Logic for Layered Control Systems.  In: The 18th Asia-Pacific Software Engineering Conference (APSEC 2011), Ho Chi Minh, Vietnam.