A generic framework: from modeling to code

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 : Model-driven development (MDD) is a very popular technique in the area of software development, but this technique is criticized due to lack of a formal semantics. MDD is used for large-scale system development using semi-formal techniques like UML (Unified Modeling Language), which are not amenable to formal analysis and consistency checking. Formal methods with MDD may provide an assurance of correctness of the system. This paper advocates an approach to building generic framework for rigorous MDD that is based on combining semi-formal notations with formal modeling languages, correctness of the system using model checker and automatic code generation from the verified formal specification. The main objective of this work is to apply model-driven techniques and tools with formal verification and its code generation for designing critical systems. An assessment of the proposed framework is given through a case study, relative to the development of a cardiac pacemaker system.
Type de document :
Article dans une revue
Innovations in Systems and Software Engineering (ISSE), Springer London, 2011, pp.1-9. 〈http://dx.doi.org/10.1007/s11334-011-0165-0〉
Liste complète des métadonnées

Contributeur : Neeraj Kumar Singh <>
Soumis le : mercredi 2 novembre 2011 - 18:26:50
Dernière modification le : mardi 24 avril 2018 - 13:32:53


  • HAL Id : inria-00637761, version 1



Dominique Méry, Neeraj Kumar Singh. A generic framework: from modeling to code. Innovations in Systems and Software Engineering (ISSE), Springer London, 2011, pp.1-9. 〈http://dx.doi.org/10.1007/s11334-011-0165-0〉. 〈inria-00637761〉



Consultations de la notice