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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Pacemaker Challenge (2007). http://sqrl.mcmaster.ca/pacemaker.htm
Interactive Prover Reference Manual 3.7 (2013). http://www.atelierb.eu/ressources/DOC/english/prover-reference-manual.pdf
iUML (2013). http://wiki.event-b.org/index.php/IUML-B
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer 12(6), 447–466 (2010)
Back, R.-J., Kurki-Suonio, R.: Decentralization of Process Nets with Centralized Control. In: Symposium on Principles of Distributed Computing, pp. 131–142. ACM, Montreal (1983)
Barold, S.S., Stroobandt, R., Sinnaeve, A.F.: Cardiac Pacemakers and Resynchronization Step-by-Step: an Illustrated Guide. Wiley-Blackwell (2010)
Bendisposto, J.: ProB 2.0 Developer Handbook (2014). http://nightly.cobra.cs.uni-duesseldorf.de/prob2/developer-documentation/prob-devel.pdf
Bryans, J., Fitzgerald, J., Romanovsky, A., Roth, A.: Patterns for Modelling Time and Consistency in Business Information Systems, pp. 105–114. IEEE Computer Society, Oxford (2010)
Butler, M., Falampin, J.: An Approach to Modelling and Refining Timing Properties in B. In: Proceedings of Workshop on Refinement of Critical Systems (RCS) (January 2002)
Cansell, D., Méry, D., Rehm, J.: Time Constraint Patterns for Event B Development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140–154. Springer, Heidelberg (2006)
Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT Solvers for Rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194–207. Springer, Heidelberg (2012)
Gomes, A.O., Oliveira, M.: Formal Development of a Cardiac Pacemaker: From Specification to Code. In: Davies, J. (ed.) SBMF 2010. LNCS, vol. 6527, pp. 210–225. Springer, Heidelberg (2011)
Jee, E., Wang, S., Kim, J.K., Lee, J., Sokolsky, O., Lee, I.: A Safety-Assured Development Approach for Real-Time Software. In: The Proceedings of the 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pp. 133–142 (August 2010)
Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and Verification of a Dual Chamber Implantable Pacemaker. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188–203. Springer, Heidelberg (2012)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Macedo, H., Larsen, P., Fitzgerald, J.: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 181–197. Springer, Heidelberg (2008)
Méry, D., Singh, N.K.: Pacemaker’s Functional Behaviors in Event-B. Research Report inria-00419973 (2009)
Rehm, J.: From Absolute-Timer to Relative-Countdown: Patterns for Model-Checking (May 2008) (Unpublished)
Sarshogh, M.R.: Extending Event-B with Discrete Timing Properties. PhD thesis, University of Southampton (2013)
Savicks, V., Butler, M., Colley, J.: Co-simulating Event-B and Continuous Models via FMI. In: 2014 Summer Computer Simulation Conference, Society for Modeling & Simulation International (SCS) (July 2014)
Sulskus, G., Poppleton, M., Rezazadeh, A.: Example Event-B project (2014). http://users.ecs.soton.ac.uk/gs6g10/SimplifiedPMExample.zip
Sulskus, G., Poppleton, M., Rezazadeh, A.: An Investigation into Event-B Methodologies and Timing Constraint Modelling. Mini-Thesis, University of Southampton (2014)
Wang, J.: Handbook of Finite State Based Models and Applications. Discrete Mathematics and Its Applications. Chapman and Hall/CRC (2012)
Yang, F., Jacquot, J.-P.: Scaling Up with Event-B: A Case Study. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 438–452. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Sulskus, G., Poppleton, M., Rezazadeh, A. (2015). An Interval-Based Approach to Modelling Time in Event-B. In: Dastani, M., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2015. Lecture Notes in Computer Science(), vol 9392. Springer, Cham. https://doi.org/10.1007/978-3-319-24644-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-24644-4_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24643-7
Online ISBN: 978-3-319-24644-4
eBook Packages: Computer ScienceComputer Science (R0)