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.
|
PDF
280Kb |
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.
| Item Type: | Book Section |
|---|---|
| Subjects: | Event-B 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
-
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
