creators_name: Iliasov, Alexei creators_name: Laibinis, Linas creators_name: Troubitsyna, Elena creators_name: Romanovsky, Alexander creators_name: Latvala, Timo creators_id: "Alexei Iliasov" creators_id: Linas.Laibinis@abo.fi creators_id: Elena.Troubitsyna@abo.fi creators_id: alexander.romanovsky@ncl.ac.uk type: book_section datestamp: 2012-03-30 14:10:28 lastmod: 2012-03-30 14:10:28 metadata_visibility: show title: Augmenting Event-B Modelling with Real-Time Verification ispublished: pub subjects: Event-Bsemantics subjects: Refinement subjects: deploy_tooldev_modelc subjects: deploy_tooldev_rodinplugins subjects: rt_modelling full_text_status: public abstract: Abstract—A large number of dependable embedded systems have stringent real-time requirements imposed on them. Analysis of their real-time behaviour is usually conducted at the implementation level. However, it is desirable to obtain an evaluation of real-time properties early at the development cycle, i.e., at the modelling stage. In this paper we present an approach to augmenting Event-B modelling with verification of real-time properties in Uppaal. We show how to extract a process-based view from an Event-B model that together with introducing time constraints allows us to obtain a timed automata model – an input model of Uppaal. We illustrate the approach by development and verification of the data processing software of the BepiColombo Mission. date_type: published publisher: ACM pages: 7 refereed: TRUE book_title: Proc. of Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches held in conjunction with ICSE 2012. 2 June 2012, Zurich, Switzerland. citation: Iliasov, Alexei and Laibinis, Linas and Troubitsyna, Elena and Romanovsky, Alexander and Latvala, Timo Augmenting Event-B Modelling with Real-Time Verification. In: Proc. of Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches held in conjunction with ICSE 2012. 2 June 2012, Zurich, Switzerland. ACM. document_url: http://deploy-eprints.ecs.soton.ac.uk/385/1/main2.pdf