--- 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.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - Yuliya.Prokhorova@abo.fi - Linas.Laibinis@abo.fi - Elena.Troubitsyna@abo.fi - ~ - ~ creators_name: - family: Prokhorova given: Yuliya honourific: '' lineage: '' - family: Laibinis given: Linas honourific: '' lineage: '' - family: Troubitsyna given: Elena honourific: '' lineage: '' - family: Varpaaniemi given: Kimmo honourific: '' lineage: '' - family: Latvala given: Timo honourific: '' lineage: '' data_type: ~ date: 2011 date_type: published datestamp: 2012-06-29 07:54:19 department: ~ dir: disk0/00/00/04/05 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 405 event_dates: ~ event_location: 'Ho Chi Minh, Vietnam' event_title: The 18th Asia-Pacific Software Engineering Conference (APSEC 2011) event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: ~ full_text_status: none funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: ~ item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2012-06-29 07:54:19 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: 49-56 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: [] publication: ~ publisher: ~ refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 14 series: ~ skill_areas: [] source: ~ status_changed: 2012-06-29 07:54:19 subjects: - Event-Bsemantics - Refinement - deploy_industrial_space - deploy_method_proof - deploy_method_resil - examples succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Derivation and Formal Verification of a Mode Logic for Layered Control Systems type: conference_item userid: 20 volume: ~