Model-Driven Engineering, Verification, and Validation
Integrating Verification and Validation in MDE
A satellite event of MODELS 2014
September 30th, Valencia, Spain
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 im- portance 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 per- spectives for the formalization and the automation of verification and validation (V&V) tasks, like testing, consistency or refinement confor- mance checking and so on. On the other hand, the growing complexity of models and of model transformations requires efficient techniques for V&V in the context of MDE. The 2014 edition of the workshop on model-driven engineering, verification, and validation (MoDeVVa) offers a forum for researchers and practitioners who are working on V&V and MDE. The main goals of the workshop are to identify, discuss, and elaborate mutual impacts of MDE and V&V. This year, following the keynote presentation given by Marsha Chechik in the 2013 edition, we would like to put a special focus on modeling and reasoning in the presence of incompleteness, underspecification and the unknown.
The workshop will start with a keynote by Markus Völter.
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 composition rules to support compositionality?
- how to model model transformations to guaranty the preservation of properties of the models?
- how to model the dependencies between fonctional and extra-fonctional requirements?
Abstraction and refinement are also usual 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 their conformance be checked?
- how to keep such models in sync?
In addition to these core issues, the keynote presentation given by Marsha Chechik at MoDeVVa last year compels us to put an emphasis on modeling and reasoning in the presence of incompleteness, underspecification and the unknown:
- How to model the unknown?
- How to make users aware about the incompleteness of their models?
- How to measure the incompleteness?
- How to verity incomplete models?
- How to handle approximation versus abstraction?
Additionally, many verification techniques (e.g. testing, bounded model checking) are inherently incomplete. For them, we would like to find adequate models to characterize their incompleteness:
- How to model incomplete verification?
- How trustful is incomplete verification?
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)
- Frédéric Boulanger
- Michalis Famelis
- Daniel Ratiu