Name
Title | ||
|---|---|---|
Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation. |
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-33600-8_31 | ABZ |
Keywords | DocType | Volume |
Hemodialysis machine,Event-B,Validation,Visualisation,iUML-B,BMotion Studio,Co-Simulation | Conference | 9675 |
ISSN | Citations | PageRank |
0302-9743 | 9 | 0.55 |
References | Authors | |
4 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thai Son Hoang | 1 | 461 | 35.14 |
| Colin F Snook | 2 | 53 | 11.42 |
| Lukas Ladenberger | 3 | 62 | 5.41 |
| Michael Butler | 4 | 1768 | 104.74 |