Hemodialysis machine in hybrid Event-B
R Banach - Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th …, 2016 - Springer
The hemodialysis machine case study is examined in Hybrid Event-B (an extension of Event-
B that includes provision for continuously varying behaviour as well as the usual discrete …
B that includes provision for continuously varying behaviour as well as the usual discrete …
Modelling a hemodialysis machine using algebraic state-transition diagrams and B-like methods
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 …
conference. The specification was carried out by a coupling of Algebraic State-Transition …
Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion studio, and co-simulation
TS Hoang, C Snook, L Ladenberger… - … , Alloy, B, TLA, VDM, and Z …, 2016 - Springer
We present a formal specification of a hemodialysis machine (HD machine) using Event-B.
We model the HD machine using iUML-B state-machines and class diagrams and build a …
We model the HD machine using iUML-B state-machines and class diagrams and build a …
[HTML][HTML] Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset
We present a formal specification and analysis of a haemodialysis machine (HD machine) in
Event-B using the Rodin Toolset. The medical device domain is a particularly complex …
Event-B using the Rodin Toolset. The medical device domain is a particularly complex …
The hemodialysis machine case study
A Mashkoor - Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th …, 2016 - Springer
This documents presents a description of a case study concerning the control of a
hemodialysis (HD) machine. It provides an overview of the requirements and the design of …
hemodialysis (HD) machine. It provides an overview of the requirements and the design of …
The landing gear case study in hybrid Event-B
R Banach - International Conference on Abstract State Machines …, 2014 - Springer
A case study problem based on a set of aircraft landing gear is examined in Hybrid Event-B
(an extension of Event-B that includes provision for continuously varying behaviour as well …
(an extension of Event-B that includes provision for continuously varying behaviour as well …
[HTML][HTML] Core hybrid Event-B I: single hybrid Event-B machines
Faced with the increasing need for correctly designed hybrid and cyber-physical systems
today, the problem of including provision for continuously varying behaviour as well as the …
today, the problem of including provision for continuously varying behaviour as well as the …
Problem decomposition and sub-model reconciliation of control systems in Event-B
S Yeganefard, M Butler - 2013 IEEE 14th International …, 2013 - ieeexplore.ieee.org
To break the complexity of the formalisation process, we propose to model a functional
requirement document of a control system as composeable monitored, controlled, mode and …
requirement document of a control system as composeable monitored, controlled, mode and …
[PDF][PDF] Towards a cookbook for modelling and refinement of control problems
M Butler - 2009 - academia.edu
This document is a attempt to develop some guidelines on modelling control problems in
Event-B. It is influenced in part by the Problem Frame approach of identifying phenomenon …
Event-B. It is influenced in part by the Problem Frame approach of identifying phenomenon …
Formal refinement and partitioning of a fuel pump system for small aircraft in hybrid Event-B
R Banach - 2016 10th International Symposium on Theoretical …, 2016 - ieeexplore.ieee.org
A case study centred on a fuel supply system for a small aircraft is presented in Hybrid Event-
B, an extension of conventional Event-B that allows for the modelling and verification of …
B, an extension of conventional Event-B that allows for the modelling and verification of …