A user-oriented approach to integrate formal verification activity for DSML

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

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

Formal methods based verification activity of safety critical embedded systems has produced very promising results in the industrial context and raised the interest of system designers up to the application of these technologies in real size projects. However, these methods usually rely on specific verification 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 powerful methods. We propose an approach which introduces different steps to integrate verification tasks for a new DSML and explains the interactions between concerned actors. 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: Index Terms-Verification; Formal methods; Domain specific modeling language (DSML); Model checking

Domaines: Informatique [cs]; Systèmes embarqués

Faiez Zalila, Xavier Crégut, Marc Pantel. A user-oriented approach to integrate formal verification activity for DSML. Embedded Real Time Software and Systems (ERTS2014), Feb 2014, Toulouse, France. ⟨hal-02272341⟩