creators_name: Dotti, Fernando creators_name: Iliasov, Alexei creators_name: Riberiro, Leila creators_name: Romanovsky, Alexander creators_id: Fernando Luis Dotti creators_id: "Alexei Iliasov" creators_id: alexander.romanovsky@ncl.ac.uk type: conference_item datestamp: 2009-09-22 07:20:12 lastmod: 2010-04-19 15:05:57 metadata_visibility: show title: Modal Systems: Specification, Refinement and Realisation ispublished: pub subjects: Refinement subjects: deploy_method_comp subjects: deploy_method_resil full_text_status: public pres_type: paper abstract: Operation modes are useful structuring units that facilitate design of several safety-critical systems such as such as avionic, transportation and space systems. Although some support to the construction of modal systems can be found in the literature, modelling abstractions for the formal specification, analysis and correct construction of modal systems are still lacking. This paper discusses existing support for the construction of modal systems and proposes both a formalisation and a refinement notion for modal systems. A modal system, specified using the proposed abstractions, can be realised using different specification languages. Complementing the contribution, we define the requirements for an Event-B model to realise a modal system specification. A case study illustrates the proposed approach. date: 2009 date_type: published event_title: International Conference on Formal Engineering Methods - ICFEM 09 event_location: Rio de Janeiro, Brazil event_dates: December 9 -12, 2009 event_type: conference refereed: TRUE citation: Dotti, Fernando and Iliasov, Alexei and Riberiro, Leila and Romanovsky, Alexander (2009) Modal Systems: Specification, Refinement and Realisation. In: International Conference on Formal Engineering Methods - ICFEM 09 , December 9 -12, 2009, Rio de Janeiro, Brazil. document_url: http://deploy-eprints.ecs.soton.ac.uk/153/1/paper105-ICFEM09.pdf