| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
An Interval-Based Approach to Modelling Time in Event-B
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.
Cited literature [23 references]
https://hal.inria.fr/hal-01446607
Contributor : Hal Ifip <>
Submitted on : Thursday, January 26, 2017 - 10:43:45 AM
Last modification on : Saturday, June 8, 2019 - 2:20:03 PM
Long-term archiving on: : Friday, April 28, 2017 - 5:52:05 AM
Contributor : Hal Ifip <>
Submitted on : Thursday, January 26, 2017 - 10:43:45 AM
Last modification on : Saturday, June 8, 2019 - 2:20:03 PM
Long-term archiving on: : Friday, April 28, 2017 - 5:52:05 AM
File
978-3-319-24644-4_20_Chapter.p...
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License