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. 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, we would like to put a special focus on modeling and verification and validation of cyber-physical systems (CPS).
Scope
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?
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?
In addition to the core issues of MoDeVVa, we would like to put an emphasis in this year on the verification and validation in context of the interaction between computers and the physical world typical realized in terms of cyber-physical systems (CPS). Therefore, we especially invite papers dealing with one of the following or similar questions:
how can verification and validation be applied in the cross-disciplinary context of CPS?
how can we specify and prove properties that span across different heterogeneous models that belong to different engineering domains?
how to verify and validate heterogeneous model transformations for CPS?
what are appropriate ways for decomposing CPS models for the purpose of V\&V?
Objectives
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)
Organizers
Michalis Famelis, University of Toronto, Canada
Daniel Ratiu, Siemens, Munich, Germany
Martina Seidl, Johannes Kepler University Linz, Austria
Gehan Selim, Queens University, Kingston, Canada
MoDeVVa Organizers email.