title: Augmenting Event-B Modelling with Real-Time Verification creator: Iliasov, Alexei creator: Laibinis, Linas creator: Troubitsyna, Elena creator: Romanovsky, Alexander creator: Latvala, Timo subject: Event-B subject: Refinement subject: Model construction subject: Rodin plug-ins subject: Real-time systems description: 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. publisher: ACM type: Book Section type: PeerReviewed format: application/pdf identifier: http://deploy-eprints.ecs.soton.ac.uk/385/1/main2.pdf identifier: 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. relation: http://deploy-eprints.ecs.soton.ac.uk/385/