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
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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.
Liste complète des métadonnées
Contributor : Dominique Méry <>
Submitted on : Wednesday, November 2, 2011 - 6:17:24 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM




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



Record views