Research project P6/39 (Research action P6)
Software-intensive systems are among the most complex artefacts ever built: they undergo a multitude of constantly changing requirements, they interact with a variety of users and systems, they are composed of many communicating and heterogeneous components, they must be able to adapt quickly to changing technologies, and they often exist in many different variants that live in parallel.
In the development of such systems, the use of rigorous models and analysis methods is essential to make sure that the software satisfies its requirements and exhibits the desired properties (e.g., safety, security, reliability, consistency). At the same time, in order to adapt to the constantly changing requirements and technology, these systems must be able to evolve over time, without breaking their essential properties.
Our research focusses on the development, integration and extension of state-of-the-art languages, formalisms and techniques for modelling and verifying dependable software systems and supporting the evolution of these systems.
In this project, we adopt a broad definition of Model Driven Engineering (MDE) as an approach that promotes the use of models (in a large sense) as primary driving assets in all aspects of software engineering, including requirements analysis, system design, platform and language definition, definition of mappings among artefacts, but also data modelling, design analysis, tool specification and product family development.
Formal modelling and verification (FMV) provides an invaluable contribution to MDE, by providing tools and techniques to (de)compose models into other models; to detect and resolve inconsistencies in and between models; to refine, transform and synthesize models while keeping them consistent; to abstract models from more detailed descriptions, and to build verification methods and tools.
Increased separation of concerns as advocated by the Aspect Oriented Software Development (AOSD) community is beneficial to software evolution, as it enables different concerns to evolve independently. Paradoxically, however, separating the software in different concerns leads to a multitude of different models that have subtle interactions and have to be kept consistent when either of them evolves. Therefore, combining AOSD and MDE introduces new challenges.
Through synergy and cross-fertilization of our expertise in model-driven engineering, formal methods and verification, software evolution and AOSD, we propose to advance the state of the art in each of these domains, by conducting:
• Advanced research on programming and modelling languages in which we can model and implement software and express relevant properties about the software under construction while enabling and supporting the automated verification of these relevant properties in the initial development and after evolution steps.
• Novel research on rigorous methods and techniques to construct, combine and verify models and programs in an MDE/AOSD context. Our objective is to provide efficient techniques and methods to transform models and to check, guarantee or achieve consistency between models through scalable verification techniques.
• Novel research on model evolution, with a dedicated focus on the study of techniques to co-evolve and restructure models, and the ability to adapt verification techniques to the context of evolving models. Our objective is to provide support to assess the change impact on, and synchronize other models with, a model that has evolved or has been restructured, and to incrementally verify properties of evolved models rather than reverifying the entire model.
This consortium combines the leading Belgian research teams in software engineering, with recognised scientific excellence in model-driven engineering, software evolution, formal modelling and verification and aspect-oriented software development. The long term objective of our network is to strengthen existing collaborations and forge new links between those teams, and to leverage and disseminate our research expertise in this domain at a European level.
