Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods

Thomas Fayolle, Marc Frappier, Frédéric Gervais, Régine Laleau
Case Study Printed Abstract Cite Source
Type
Conference paper
Publication
5th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'16)

Abstract

This paper presents the specification of the hemodialysis case study, proposed by ABZ'16 conference. The specification was carried out by a coupling of Algebraic State-Transition Diagrams (ASTD) and B-like methods. astd are a graphical notation, based on automata and process algebra operators. They provide an easy-to-read specification of the dynamic behaviour of the system. The data model is specified using the Event-B language. The system is incrementally designed using extended refinement of both methods.

Reference

% BibTex
@InProceedings{10.1007/978-3-319-33600-8_33,
author="Fayolle, Thomas
and Frappier, Marc
and Gervais, Fr{\'e}d{\'e}ric
and Laleau, R{\'e}gine",
editor="Butler, Michael
and Schewe, Klaus-Dieter
and Mashkoor, Atif
and Biro, Miklos",
title="Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods",
booktitle="Abstract State Machines, Alloy, B, TLA, VDM, and Z",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="394--408",
isbn="978-3-319-33600-8"
}

Sources

  • Used formal method: Algebraic State-Transition Diagrams (ASTD)

    For more information, please contact the authors

ABZ'16

Related