Skip to main content
SpringerLink
Log in
Book cover

International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z

ABZ 2016: Abstract State Machines, Alloy, B, TLA, VDM, and Z pp 376–393Cite as

Hemodialysis Machine in Hybrid Event-B

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9675))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 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. 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. 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. 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. 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. 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

  1. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  2. Ahmad, S.: Manual of Clinical Dialysis. Springer, US (2009)

    Book  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Banach, R.: Hemodialysis Case Study in Hybrid Event-B Web Site (2015). http://www.cs.man.ac.uk/banach/some.pubs/ABZ2016HemodialysisCaseStudy/

  5. Banach, R.: The landing gear system in multi-machine hybrid event-B. Int. J. Softw. Tools Tech. Trans., pp. 1–24 (2015, to appear)

    Google Scholar 

  6. 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)

    Article  Google Scholar 

  7. Banach, R., Butler, M., Qin, S., Zhu, H.: Core Hybrid Event-B II: Multiple Cooperating Hybrid Event-B Machines (Submitted) (2015)

    Google Scholar 

  8. Banach, R., Jeske, C.: Retrenchment and refinement interworking: the tower theorems. Math. Struct. Comp. Sci. 25(1), 135–202 (2015)

    Article  MathSciNet  Google Scholar 

  9. Banach, R., Jeske, C., Poppleton, M.: Composition mechanisms for retrenchment. J. Logic Algebraic Program. 75, 209–229 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  10. Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comp. Program. 67, 301–329 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  11. Crnkovic, I., Larsson, M.: Building Reliable Component-based Software Systems. Artech House, Norwood (2002)

    MATH  Google Scholar 

  12. Daugirdas, J., Blake, P., Ing, T.: Handbook of Dialysis. Wolters Kluwer, New York (2007)

    Google Scholar 

  13. Harris, D., Elder, G., Kairaitis, G., Rangan, G.: Basic Clinical Dialysis. McGraw Hill, Sydney (2005)

    Google Scholar 

  14. Heineman, G., Councill, W.: Component-Based Software Engineering: Putting the Pieces Together. Addison Wesley, Boston (2001)

    Google Scholar 

  15. Kallenbach, J., Gutch, C., Stoner, M., Corea, A.: Review of Hemodialysis for Nurses and Dialysis Personnel. Elsevier Mosby, Philadelphia (2005)

    Google Scholar 

  16. 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)

    Google Scholar 

  17. Nissenson, A., Fine, R.: Handbook of Dialysis Therapy. Saunders Elsevier, Philadelphia (2008)

    Google Scholar 

  18. Somaia, Z.: Component-Based Software Development. Lambert Academic Publishing, Germany (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Manchester, Oxford Road, Manchester, M13 9PL, UK

    Richard Banach

Authors
  1. Richard Banach
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Richard Banach .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Software Competence Center, Hagenberg, Austria

    Klaus-Dieter Schewe

  3. Software Competence Center, Hagenberg, Austria

    Atif Mashkoor

  4. Software Competence Center, Hagenberg, Austria

    Miklos Biro

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation