Modelling the Haemodialysis Machine with Circus

Artur Oliveira Gomes, Andrew Butterfield
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 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.

Document

Reference

% BibTex
@InProceedings{10.1007/978-3-319-33600-8_34,
author="Gomes, Artur O.
and Butterfield, Andrew",
editor="Butler, Michael
and Schewe, Klaus-Dieter
and Mashkoor, Atif
and Biro, Miklos",
title="Modelling the Haemodialysis Machine with Circus",
booktitle="Abstract State Machines, Alloy, B, TLA, VDM, and Z",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="409--424",
isbn="978-3-319-33600-8"
}

Sources

  • Used formal method: Circus

    For more information, please contact the authors

ABZ'16

Related