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
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.
Type de document :
Article dans une revue
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 12 (1), pp.15. 〈10.1145/2406336.2406351〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00637756
Contributeur : Dominique Méry <>
Soumis le : mercredi 2 novembre 2011 - 18:17:24
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

358