2012 First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA 2012)
Download PDF

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.
Like what you’re reading?
Already a member?
Get this article FREE with a new membership!

Related Articles