Trustable Formal Specification for Software Certification

Dominique Méry 1 Neeraj Kumar Singh 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Formal methods have emerged as an alternative approach to ensuring quality and correctness of high confidence medical devices, overcoming limitations of traditional validation techniques such as simulation and testing. In this paper, we propose a new methodology to obtain certification assurance for complex medical devices design, based on the use of formal methods. The methodology consists of five main phases: first, informal requirements, resulting in a structured version of the requirements, where each fragment is classified according to a fixed taxonomy. In the second phase, informal requirements are represented in formal modeling language, with a precise semantics, and enriched with invariants and temporal constraints. The third phase consists of refinement-based formal verification to test the internal consistency and correctness of the specifications. The fourth phase is the process of determining the degree to which a formal model is an accurate representation of the real world from the perspective of the intended uses of the model using model-checker. Last phase is used to animate the formal model with real-time data set instead of toy-data, and offers a simple way for specifiers to build a domain specific visualization that can be used by domain experts to check whether a formal specification corresponds to their expectations. Furthermore, we show the effectiveness of this methodology for modeling of a cardiac pacemaker.
Type de document :
Communication dans un congrès
T. Margaria and B. Ste. 4th International Symposium On Leveraging Applications of Formal Methods - ISOLA 2010, Oct 2010, Heraklion, Crete, Greece. Springer, 6416, pp.312-326, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-16561-0_31〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00540008
Contributeur : Neeraj Kumar Singh <>
Soumis le : jeudi 25 novembre 2010 - 19:34:48
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Trustable Formal Specification for Software Certification. T. Margaria and B. Ste. 4th International Symposium On Leveraging Applications of Formal Methods - ISOLA 2010, Oct 2010, Heraklion, Crete, Greece. Springer, 6416, pp.312-326, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-16561-0_31〉. 〈inria-00540008〉

Partager

Métriques

Consultations de la notice

107