%0 Conference Proceedings
%T An Interval-Based Approach to Modelling Time in Event-B
%+ University of Southampton
%A Sulskus, Gintautas
%A Poppleton, Michael
%A Rezazadeh, Abdolbaghi
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 6th Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Mehdi Dastani
%Y Marjan Sirjani
%I Springer
%3 Fundamentals of Software Engineering
%V LNCS-9392
%P 292-307
%8 2015-04-22
%D 2015
%R 10.1007/978-3-319-24644-4_20
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01446607/document
%2 https://inria.hal.science/hal-01446607/file/978-3-319-24644-4_20_Chapter.pdf
%L hal-01446607
%U https://inria.hal.science/hal-01446607
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-LNCS-9392
%~ IFIP-FSEN