Skip to Main content Skip to Navigation
New interface
Journal articles

Formal Specification of Medical Systems by Proof-Based Refinement

Dominique Méry 1, 2 Neeraj Kumar Singh 1, 3 
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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
Abstract : Formal methods have emerged as an alternative approach to ensuring quality and correctness of highly critical systems, overcoming limitations of traditional validation techniques such as simulation and testing. We propose a refinement-based methodology for complex medical systems design, which possesses all the required key features. A refinement-based combined approach of formal verification, model validation using a model-checker and refinement chart is proposed in this methodology for designing a high-confidence medical device. Furthermore, we show the effectiveness of this methodology for the design of a cardiac pacemaker system.
Complete list of metadata
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Wednesday, November 2, 2011 - 6:17:24 PM
Last modification on : Friday, February 11, 2022 - 3:11:21 AM



Dominique Méry, Neeraj Kumar Singh. Formal Specification of Medical Systems by Proof-Based Refinement. ACM Transactions on Embedded Computing Systems (TECS), 2013, 12 (1), pp.15. ⟨10.1145/2406336.2406351⟩. ⟨inria-00637756⟩



Record views