nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Hemodialysis Machine in Hybrid Event-B

verfasst von : Richard Banach

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

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation

Nächstes Kapitel Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods

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.

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.

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.

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.

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.

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

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

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

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

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

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

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

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)

Titel: Hemodialysis Machine in Hybrid Event-B
verfasst von: Richard Banach
Verlag: Springer International Publishing
Buch: Abstract State Machines, Alloy, B, TLA, VDM, and Z
Print ISBN: 978-3-319-33599-5

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

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

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"