Critical systems development methodology using formal techniques

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
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 the quality and correctness of the high con - dence critical systems, overcoming limitations of the traditional validation techniques such as simulation and testing. This paper presents a methodology for developing the critical systems from requirement analysis to automatic code generation with standard safety assessment approach. This methodology combines the re nement approach with various tools including veri cation tool, model checker tool, real-time animator and nally, produces the source code into many languages using automatic code generation tools. This approach intends as a contribute to further the use of formal techniques for developing critical systems with high integrity and to verify the complex properties, which help to discover the potential problems. Assessment of the proposed methodology is given through developing a standard case study: the cardiac pacemaker.
Liste complète des métadonnées
Contributor : Dominique Méry <>
Submitted on : Wednesday, October 31, 2012 - 1:13:26 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM




Dominique Méry, Neeraj Kumar Singh. Critical systems development methodology using formal techniques. 3rd International Symposium on Information and Communication Technology - SoICT 2012, Aug 2012, Ha Long, Vietnam. pp.3-12, ⟨10.1145/2350716.2350720⟩. ⟨hal-00747305⟩



Record views