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
|Deposited By:||Prof A Romanovsky|
|Deposited On:||30 Mar 2012 14:10|
|Last Modified:||30 Mar 2012 14:10|
Available Versions of this Item
Augmenting Event-B Modelling with Real-Time Verification. (deposited 30 Mar 2012 14:07)
- Augmenting Event-B Modelling with Real-Time Verification. (deposited 30 Mar 2012 14:10) [Currently Displayed]
Repository Staff Only: item control page