Modelling the haemodialysis machine with Circus

We present a formal model of aspects of the haemodialysis machine case study using the Circus speci cation 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. 1