creators_name: Dotti, Fernando creators_name: Iliasov, Alexei creators_name: Romanovsky, Alexander creators_id: Fernando Luis Dotti creators_id: "Alexei Iliasov" creators_id: alexander.romanovsky@ncl.ac.uk type: other datestamp: 2009-07-08 15:31:36 lastmod: 2010-04-19 15:05:56 metadata_visibility: show title: Specifying Modal Systems using Event-B ispublished: unpub subjects: deploy_method_comp subjects: deploy_method subjects: Event-Bsemantics full_text_status: public pres_type: paper abstract: Several safety-critical systems, such as avionic, transportation and space systems, use the notion of operation modes. Operation modes are useful structuring units that facilitate design, specially if used with state-based formal methods. However, modelling abstractions to support the specification, analysis and correct construction of modal systems are still lacking. The contribution of this paper is twofold: (i) modal systems and modal systems refinement are discussed and formalized; (ii) the relation of a modal system specification with an Event-B model is discussed, showing how to demonstrate that the behaviour of an Event-B model can satisfy a modal system. publisher: (Technical report) event_title: Newcastle University event_location: event_dates: event_type: other refereed: FALSE citation: Dotti, Fernando and Iliasov, Alexei and Romanovsky, Alexander Specifying Modal Systems using Event-B. (Technical report). (Unpublished) document_url: http://deploy-eprints.ecs.soton.ac.uk/134/1/modesFM.pdf