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

Thai Son Hoang, Colin F. Snook, Lukas Ladenberger, Michael J. Butler
Case Study Digital Printed Abstract View Cite Source
Type
Conference paper
Publication
5th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'16)

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

Document

Reference

% BibTex
@InProceedings{10.1007/978-3-319-33600-8_31,
author="Hoang, Thai Son
and Snook, Colin
and Ladenberger, Lukas
and Butler, Michael",
editor="Butler, Michael
and Schewe, Klaus-Dieter
and Mashkoor, Atif
and Biro, Miklos",
title="Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation",
booktitle="Abstract State Machines, Alloy, B, TLA, VDM, and Z",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="360--375",
isbn="978-3-319-33600-8"
}

Sources

  • Used formal method: Event-B

  • Resources and tools: ProB

    For more information, please contact the authors

ABZ'16

Related