%A Alexei Iliasov
%A Linas Laibinis
%A Elena Troubitsyna
%A Alexander Romanovsky
%A Timo Latvala
%T Augmenting Event-B Modelling with Real-Time Verification
%X 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.
%I ACM
%L deploy385
%B Proc. of Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches held in conjunction with ICSE 2012. 2 June 2012, Zurich, Switzerland.

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>