Formal MDE-based tool development

Abstract

Model-driven engineering (MDE) focuses on creating and exploiting (specific) domain models. It is common to use domain-specific languages (DSL) to describe the concrete elements of such models. MDE tools can easily build DSLs, although it is not clear how to capture dynamic semantics as well as formally verify properties. Formal methods are a well-known solution for providing correct software, but human-machine interaction is usually not addressed. Several industries, particularly the safety-critical industries, use mathematical representations to deal with their problem domains. Such DSLs are difficult to capture, using just MDE tools for instance, because they have specific semantics to provide the desired (core) expected behavior. Thus, we propose a rigorous methodology to create GUI (Graphical User Interface) based DSLs formal tools. We aim at providing a productive and trustworthy development methodology to safety critical industries.