@incollection{deploy385,
       booktitle = {Proc. of Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches held in conjunction with ICSE 2012. 2 June 2012, Zurich, Switzerland.},
           title = {Augmenting Event-B Modelling with Real-Time Verification},
          author = {Alexei Iliasov and Linas Laibinis and Elena Troubitsyna and Alexander Romanovsky and Timo Latvala},
       publisher = {ACM},
             url = {http://deploy-eprints.ecs.soton.ac.uk/385/},
        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.}
}

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