TY - CHAP ID - deploy385 UR - http://deploy-eprints.ecs.soton.ac.uk/385/ A1 - Iliasov, Alexei A1 - Laibinis, Linas A1 - Troubitsyna, Elena A1 - Romanovsky, Alexander A1 - Latvala, Timo N2 - 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. PB - ACM TI - Augmenting Event-B Modelling with Real-Time Verification AV - public EP - 7 T2 - Proc. of Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches held in conjunction with ICSE 2012. 2 June 2012, Zurich, Switzerland. ER -