Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Hemodialysis Machine in Hybrid Event-B

Author : Richard Banach

Published in: Abstract State Machines, Alloy, B, TLA, VDM, and Z

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation
next chapter Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods
Footnotes
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].
 
Literature
1.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
2.
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)CrossRef
4.
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)
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)CrossRef
7.
Banach, R., Butler, M., Qin, S., Zhu, H.: Core Hybrid Event-B II: Multiple Cooperating Hybrid Event-B Machines (Submitted) (2015)
8.
Banach, R., Jeske, C.: Retrenchment and refinement interworking: the tower theorems. Math. Struct. Comp. Sci. 25(1), 135–202 (2015)MathSciNetCrossRef
9.
10.
Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comp. Program. 67, 301–329 (2007)MathSciNetCrossRefMATH
11.
Crnkovic, I., Larsson, M.: Building Reliable Component-based Software Systems. Artech House, Norwood (2002)MATH
12.
Daugirdas, J., Blake, P., Ing, T.: Handbook of Dialysis. Wolters Kluwer, New York (2007)
13.
Harris, D., Elder, G., Kairaitis, G., Rangan, G.: Basic Clinical Dialysis. McGraw Hill, Sydney (2005)
14.
Heineman, G., Councill, W.: Component-Based Software Engineering: Putting the Pieces Together. Addison Wesley, Boston (2001)
15.
Kallenbach, J., Gutch, C., Stoner, M., Corea, A.: Review of Hemodialysis for Nurses and Dialysis Personnel. Elsevier Mosby, Philadelphia (2005)
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)
17.
Nissenson, A., Fine, R.: Handbook of Dialysis Therapy. Saunders Elsevier, Philadelphia (2008)
18.
Somaia, Z.: Component-Based Software Development. Lambert Academic Publishing, Germany (2014)
Metadata
Title
Hemodialysis Machine in Hybrid Event-B
Author
Richard Banach
Copyright Year
2016
Book
Abstract State Machines, Alloy, B, TLA, VDM, and Z

Print ISBN: 978-3-319-33599-5

Electronic ISBN: 978-3-319-33600-8

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-33600-8_32

Premium Partner

    Image Credits