Ideal Mode Selection of a Cardiac Pacing System

Dominique Méry 1, 2 Neeraj Kumar Singh 1, 3
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 CS-YORK - Department of Computer Science [York]
Abstract : Mode transition in any inappropriate mode can be a common cause of any mishap in a complex health-care system. This paper presents an approach for formalizing and reasoning about optimal mode transition in a health-care system that uses several operating modes in various operating states. Modes are formal- ized and their relation to a state-based formalism is established through a re- finement approach. The efficiency of this approach is presented by formalizing an ideal operating mode transition of a cardiac pacemaker case study. An incre- mental approach is used to develop the system and its detailed design is verified through a series of refinements. The consequence of this approach is to improve system structuring, elicitation of system assumptions and expected functionality, as well as requirement traceability using modes in state-based modeling. Models are expressed in EVENT B modeling language and validated by a model checker tool: ProB.
Keywords : Abstract model Event-B Proof-based development Refinement Modes Pacemaker
Document type :
Conference papers
Liste complète des métadonnées
https://hal.inria.fr/hal-00862077
Contributor : Dominique Méry <>
Submitted on : Monday, September 16, 2013 - 7:49:13 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

Links full text

istex

Identifiers

Collections

INRIA | UNIV-LORRAINE | TDS-MACS | LORIA-FM | LORIA

Citation

Dominique Méry, Neeraj Kumar Singh. Ideal Mode Selection of a Cardiac Pacing System. 4th International Conference - Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management - DHM 2013 (HCI International 2013), Jul 2013, Las Vegas, United States. pp.258-267, ⟨10.1007/978-3-642-39173-6_31⟩. ⟨hal-00862077⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

440

Contact


archive-ouverte@inria.fr