Formal Verification Integration Approach for DSML

Faiez Zalila (1) , Xavier Crégut (2, 3) , Marc Pantel (2, 3)

1 IRIT - Institut de recherche en informatique de Toulouse
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 Toulouse INP - Institut National Polytechnique (Toulouse)

The application of formal methods (especially, model check- ing and static analysis techniques) for the verification of safety critical embedded systems has produced very good results and raised the inter- est of system designers up to the application of these technologies in real size projects. However, these methods usually rely on specific verifica- tion oriented formal languages that most designers do not master. It is thus mandatory to embed the associated tools in automated verification toolchains that allow designers to rely on their usual domain-specific modeling languages (DSMLs) while enjoying the benefits of these power- ful methods. More precisely, we propose a language to formally express system requirements and interpret verification results so that system designers (DSML end-users) avoid the burden of learning some formal verification technologies. Formal verification is achieved through trans- lational semantics. This work is based on a metamodeling pattern for executable DSML that favors the definition of generative tools and thus eases the integration of tools for new DSMLs

Mots clés: Translational semantics; Traceability; Verification feedback; Domain specific modeling language; Formal verification; Model checking

Domaines: Génie logiciel [cs.SE]

Faiez Zalila, Xavier Crégut, Marc Pantel. Formal Verification Integration Approach for DSML. MoDELS, Sep 2013, Miami, United States. pp.336-351, ⟨10.1007/978-3-642-41533-3_21⟩. ⟨hal-00994413⟩