Industrial deployment of system engineering methods providing high dependability and productivity


Augmenting Event-B Modelling with Real-Time Verification

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.

This is the latest version of this item.



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.

Item Type:Book Section
Methodology > Refinement
Tool developments > Model construction
Tool developments > Rodin plug-ins
Methodology > Real-time systems
ID Code:385
Deposited By: Prof A Romanovsky
Deposited On:30 Mar 2012 14:10
Last Modified:30 Mar 2012 14:10

Available Versions of this Item

Repository Staff Only: item control page

Deploy-Project - All right reserved