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

Overview & Synopsis

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.