"385","Augmenting Event-B Modelling with Real-Time Verification","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.","http://deploy-eprints.ecs.soton.ac.uk/385/","Iliasov, Alexei and Laibinis, Linas and Troubitsyna, Elena and Romanovsky, Alexander and Latvala, Timo","UNSPECIFIED","       <span class=\"person_name\">Iliasov, Alexei</span> and <span class=\"person_name\">Laibinis, Linas</span> and <span class=\"person_name\">Troubitsyna, Elena</span> and <span class=\"person_name\">Romanovsky, Alexander</span> and <span class=\"person_name\">Latvala, Timo</span>       <a href=\"http://deploy-eprints.ecs.soton.ac.uk/385/\"><em>Augmenting Event-B Modelling with Real-Time Verification.</em></a>              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.                ","\"Alexei Iliasov\" <Alexei.Iliasov@newcastle.ac.uk>,Linas.Laibinis@abo.fi,Elena.Troubitsyna@abo.fi,alexander.romanovsky@ncl.ac.uk,",""
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>