A DSL to Feedback Formal Verification Results

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

1 IRT Saint Exupéry - Institut de Recherche Technologique
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 Toulouse INP - Institut National Polytechnique (Toulouse)

The integration of early formal validation and verification (V&V) tools (model checking, static analysis, etc.) in the V&V activities for domain-specific modeling languages (DSMLs) is a key asset to improve safety and reduce development and maintenance costs. However, system designers (DSMLs end-users) expect a seamless approach embedding transparently these tools in automated toolchains while enjoying their benefits. Thus, a mandatory task for DSML designer is to feedback at the DSML level the verification results generated by these tools. This contribution highlights a domain-specific language (DSL) to describe this feedback and the associated tools that helps the DSML designer in integrating the V&V tools. A translational semantics is given — as a higher-order transformation — for this DSL in order to automatically generate a model transformation which builds verification results at the DSML level from the ones produced at the formal level.

Domaines: Informatique [cs]

Faiez Zalila, Xavier Crégut, Marc Pantel. A DSL to Feedback Formal Verification Results. 13th Model-Driven Engineering, Verification and Validation Workshop at MODELS conference 2016 (MoDeVVa 2016), Oct 2016, Saint Malo, France. pp.30--39. ⟨hal-03172263⟩