Abstract : Our work was inspired by our modelling and verification of a cardiac pacemaker, which includes concurrent aspects and a set of interdependent and cyclic timing constraints. To model timing constraints in such systems, we present an approach based on the concept of timing interval. We provide a template-based timing constraint modelling scheme that could potentially be applicable to a wide range of modelling scenarios. We give a notation and Event-B semantics for the interval. The Event-B coding of the interval is decoupled from the application logic of the model, therefore a generative design of the approach is possible. We demonstrate our interval approach and its refinement through a small example. The example is verified, model-checked and animated (manually validated) with the ProB animator.
Type de document :
Communication dans un congrès
Mehdi Dastani; Marjan Sirjani. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. Springer, Lecture Notes in Computer Science, LNCS-9392, pp.292-307, 2015, Fundamentals of Software Engineering. 〈10.1007/978-3-319-24644-4_20〉
https://hal.inria.fr/hal-01446607
Contributeur : Hal Ifip
<>
Soumis le : jeudi 26 janvier 2017 - 10:43:45
Dernière modification le : jeudi 26 janvier 2017 - 10:57:18
Document(s) archivé(s) le : vendredi 28 avril 2017 - 05:52:05
Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh. An Interval-Based Approach to Modelling Time in Event-B. Mehdi Dastani; Marjan Sirjani. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. Springer, Lecture Notes in Computer Science, LNCS-9392, pp.292-307, 2015, Fundamentals of Software Engineering. 〈10.1007/978-3-319-24644-4_20〉. 〈hal-01446607〉
