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) ProBbased 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.
CITATION STYLE
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 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9675, pp. 360–375). Springer Verlag. https://doi.org/10.1007/978-3-319-33600-8_31
Mendeley helps you to discover research relevant for your work.