We present a formal model of aspects of the haemodialysis machine case study using the Circus specification notation. We focus on building a model in which each of the software requirements (R-1–36) are represented by a Circus action. All of these act in concert with actions that model the collection of sensor data and the progress through the various therapy phases and activities. We then present how we model check the system using FDR.
CITATION STYLE
Gomes, A. O., & Butterfield, A. (2016). Modelling the haemodialysis machine with Circus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9675, pp. 409–424). Springer Verlag. https://doi.org/10.1007/978-3-319-33600-8_34
Mendeley helps you to discover research relevant for your work.