Loading...
Date
2016
Abstract
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
Supervisor
Description
peer-reviewed
Publisher
Springer
Citation
ABZ 2016 Proceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z: Lecture Notes in Computer Science (LNCS);9675, pp. 409-424
Files
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)