Abstract
The hemodialysis machine case study is examined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A broadly component based strategy is adopted, using the multi-machine and coordination facilities of Hybrid Event-B. Since, like most medical procedures, hemodialysis is under overall human control, it is largely a sequential process, with some branching to deal with exceptional circumstances. This makes for a relatively uncomplicated modelling framework, provided a model of the operator is included in order to capture the handling of exceptions.
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
Similar content being viewed by others
Notes
- 1.
In the most extreme cases, the operator or assistant undertakes a manual reinfusion of the patient when a power failure causes the equipment to halt.
- 2.
In [16] it is stated that the volumes in and out of the balance chamber are equal, but this is only true modulo the additional considerations stated here.
- 3.
Obviously, the actual, measured flow rate, cannot exceed the rate that the pump is trying to achieve. To do so would contravene the laws of thermodynamics. However, in order to assert this, we must assume that the measured flow rate is dependable.
- 4.
In reality, such a variable will be monitored discretely, with a short sampling period. But in Hybrid Event-B terms it would correspond to a pliant variable, varying piecewise smoothly.
- 5.
Since the blood pump rate is continuous, the rate must drop below 70 % of desired (R-3) before it can go into reverse (R-4), so one might conclude from the text of [16] that R-4 is redundant.
- 6.
Aside from the routine nature of the invariants, is the fact that the actual degree of required sequentiality in hemodialysis is not clearly delineated in [16].
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Ahmad, S.: Manual of Clinical Dialysis. Springer, US (2009)
Banach, R.: The landing gear case study in hybrid event-B. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 126–141. Springer, Heidelberg (2014)
Banach, R.: Hemodialysis Case Study in Hybrid Event-B Web Site (2015). http://www.cs.man.ac.uk/banach/some.pubs/ABZ2016HemodialysisCaseStudy/
Banach, R.: The landing gear system in multi-machine hybrid event-B. Int. J. Softw. Tools Tech. Trans., pp. 1–24 (2015, to appear)
Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core hybrid event-B I: single hybrid event-B machines. Sci. Comp. Program. 105, 92–123 (2015)
Banach, R., Butler, M., Qin, S., Zhu, H.: Core Hybrid Event-B II: Multiple Cooperating Hybrid Event-B Machines (Submitted) (2015)
Banach, R., Jeske, C.: Retrenchment and refinement interworking: the tower theorems. Math. Struct. Comp. Sci. 25(1), 135–202 (2015)
Banach, R., Jeske, C., Poppleton, M.: Composition mechanisms for retrenchment. J. Logic Algebraic Program. 75, 209–229 (2008)
Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comp. Program. 67, 301–329 (2007)
Crnkovic, I., Larsson, M.: Building Reliable Component-based Software Systems. Artech House, Norwood (2002)
Daugirdas, J., Blake, P., Ing, T.: Handbook of Dialysis. Wolters Kluwer, New York (2007)
Harris, D., Elder, G., Kairaitis, G., Rangan, G.: Basic Clinical Dialysis. McGraw Hill, Sydney (2005)
Heineman, G., Councill, W.: Component-Based Software Engineering: Putting the Pieces Together. Addison Wesley, Boston (2001)
Kallenbach, J., Gutch, C., Stoner, M., Corea, A.: Review of Hemodialysis for Nurses and Dialysis Personnel. Elsevier Mosby, Philadelphia (2005)
Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329–343. Springer, Heidelberg (2016)
Nissenson, A., Fine, R.: Handbook of Dialysis Therapy. Saunders Elsevier, Philadelphia (2008)
Somaia, Z.: Component-Based Software Development. Lambert Academic Publishing, Germany (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Banach, R. (2016). Hemodialysis Machine in Hybrid Event-B. 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_32
Download citation
DOI: https://doi.org/10.1007/978-3-319-33600-8_32
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)