Formal Verification Integration Approach for DSML

Abstract

The application of formal methods (especially, model checking and static analysis techniques) for the verification of safety critical embedded systems has produced very good results 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. 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 translational 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.