Models are purposeful abstractions of systems and of their environment. They can be applied at arbitrary abstraction levels for understanding complex systems, validating requirements, simulation or automatic code generation. Thus, the usage of models is of increasing importance for industrial applications. Model-Driven Engineering (MDE) is a development methodology that is based on models, meta-models, and model transformations. The shift from code or technical artifacts to software models is a key feature of MDE which opens promising perspectives for the formalization and the automation of verification and validation (V&V) tasks. On the other hand, the growing complexity of models and of model transformations requires efficient techniques for V&V in the context of MDE.
For the 2017 edition of the MoDeVVa workshop, we put an emphasis on making the V&V of MDE artifacts (e.g., models, metamodels, and model transformations) a well defined, automated, and systematic process. This includes modeling the V&V activities and composing them into workflows to increase the confidence in the generated V&V results. We are also interested in how do different V&V techniques compare with each other and with classical testing. Such comparisons can be based on several criteria, such as ease-of-use, soundness, completeness, and run-time.
Modeling is a powerful technique for handling the complexity of the design of software or hardware artifacts and of their environment. Model Driven Engineering provides efficient tools for working with models from the specification to the validation of a system. Through the systematic use of digital models, which can be processed automatically by programs, MDE offers the opportunity to validate every step in the design of a system. The first motivation for MoDeVVa is therefore the integration of verification and validation techniques into MDE.
Moreover, good models allow the design of more and more complex systems, and the complexity of the models and of the processing is growing to the point where models and MDE tools are becoming complex systems. It is therefore necessary to have efficient verification and validation techniques for models, too. The second motivation for MoDeVVa is the application of V&V techniques to MDE.
Since complexity can be handled by hierarchically breaking complex models into simpler ones, an important issue is the ability to predict the properties of the whole system from the properties of its subsystems and from the laws of combination of the subsystems. Important questions regarding hierarchical modeling are:
how to divide a model into submodels that can be realized as individually verified subsystems, integrated into a validated system?
how to model model transformations to guarantee the preservation of properties of the models?
how to model the dependencies between functional and extra-functional requirements?
Abstraction and refinement are core techniques for managing complexity:
which modeling languages are adequate to specify abstract models?
is it necessary to use semantically weak modeling languages for the first design steps, when the designers are still exploring the problem they have to solve?
how to relate models at different levels of abstraction?
how can the conformance of models at different abstraction levels be checked?
how to keep such models in sync?
Modeling and reasoning in the presence of incompleteness, underspecification and the unknown poses the following challenges:
how to model the unknown?
how to make users aware about the incompleteness of their models?
how to measure the incompleteness?
how to verify incomplete models?
how to handle approximation versus abstraction?
In addition to the core issues of MoDeVVa, we would like to put an emphasis in this year on making the V&V activities systematic in order to increase the confidence in verification results. Therefore, we especially invite papers dealing with one of the following or similar questions:
What are the synergies between different V&V activities?
Can V&V activities be aligned as a workflow to systematize and enhance the V&V process?
How do different V&V approaches compare with each other with respect to different criteria (e.g., run-time, soundness, completeness)?
Since testing is considered one of the most “user-friendly” V&V approaches, how do other approaches’ ease of use compare with that of testing?
How can V&V steps be fully automated? Steps of interest span from those that have been traditionally conducted in a purely manual manner (e.g., model and code review) to those that have been semi-automated or require some level of user intervention (e.g., test case generation and the back annotation of formal verification results in intuitive languages).
The objective of the workshop is to bring together researchers and practitioners in the domain of V&V and MDE so that key V&V issues in MDE can be identified and solved. For instance, regarding usability, V&V specialists can bring theoretical foundations and approaches that work in specific cases. MDE spe- cialists can identify common patterns in these V&V approaches and factorize them, making the concepts easier to understand and use in various applicative contexts.
The presentations and discussions should cover:
the integration of V&V approaches into MDE
the definition of V&V approaches that rely on MDE
modeling the rules for combining sub-models in order to improve compositionality
modeling conformance relations for checking the refinement of models
modeling transformations between models used for design and models used for V&V
incremental V&V (reuse as many V&V results as possible after a change in a model)
the application of the above topics to MDE itself (V&V of meta-models, models and model transformations)
continuous V&V of models
V&V of models and modeling tools (e.g. generators) for safety critical systems
using models to increase practicability of formal verification
experience reports
Ernesto Posse, Zeligsoft, Canada
Daniel Ratiu, Siemens, Germany
Gehan Selim, McMaster University, Canada
Faiez Zalila, INRIA, France
MoDeVVa Organizers email.