Abstract
We present a formal specification of a hemodialysis machine (HD machine) using Event-B. We model the HD machine using iUML-B state-machines and class diagrams and build a corresponding BMotion Studio visualisation. We focus on validation using (i) diagrams to aid the modelling of the sequential properties of the requirements, and (ii) ProB-based animation and visualisation tools to explore the system’s behaviour. Some of the safety properties involve dynamic behaviour which is difficult to verify in Event-B. For these properties we use co-simulation tools to validate against a continuous model of the physical behaviour.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Originally BMotion Studio was developed as a separate plug-in for Rodin [7].
- 2.
See jQuery selector API: http://api.jquery.com/category/selectors/.
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. 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. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)
Dassault Systemes. Catia Systems Engineering Dymola. http://www.3ds.com/products-services/catia/products/dymola (Accessed on January 2016)
FMI Steering Committee. Functional Mock-up Interface. https://www.fmi-standard.org (Accessed on January 2016)
Hoang, T.S.: An introduction to the Event-B modelling method. Industrial Deployment of System Engineering Methods, pp. 211–236. Springer, Heidelberg (2013)
Ladenberger, L.: BMotion Studio for ProB project website. http://stups.hhu.de/ProB/w/BMotion_Studio,
Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising event-B Models with B-Motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202–204. Springer, Heidelberg (2009)
Mashkoor, A.: The hemodialysis machine case study (2015). http://www.cdcc.faw.jku.at/ABZ2016/HD-CaseStudy.pdf
Savicks, V., Butler, M., Colley, J.: Co-simulating Event-B, continuous models via FMI. In: Proceedings of the 2014 Summer Simulation Multiconference, SummerSim 2014, pp. 37:1–37:8. Society for Computer Simulation International, San Diego (2014)
Savicks, V., Snook, C.: A framework for diagrammatic modelling extensions in Rodin. In: Rodin Workshop 2012, Fontainbleau (2012)
Snook, C.: Modelling control process and control mode with synchronising orthogonal state machines. In: B2011, Limerick (2011)
Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop, Toulouse, France (2014). http://eprints.soton.ac.uk/365301/
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Hoang, T.S., Snook, C., Ladenberger, L., Butler, M. (2016). Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation. In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-33600-8_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33599-5
Online ISBN: 978-3-319-33600-8
eBook Packages: Computer ScienceComputer Science (R0)