Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-simulation (Abstract)

Abstract. 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) ProB-based animation and visualisation tools to explore the system’s be- haviour. Some of the safety properties involve dynamic behaviour which is di cult to verify in Event-B. For these properties we use co-simulation tools to validate against a continuous model of the physical behaviour.

Keywords: Hemodialysis Machine, Event-B, Validation, Visualisation, iUML-B, BMotion Studio, Co-Simulation.