MOVERE: Model Driven Validation and Verification of Resilient Software Systems

Verification and Validation of software have nowadays clear meanings in the context of Model-Driven Engineering. Whereas with verification we worry about producing a set of test cases that will increase trust and find faults in an implementation – also called in the literature System Under Test (SUT) – with validation we worry about understanding if the model we are using as a reference for implementation and for extracting test cases from is sound. Validation is achieved by mechanically proving properties the model should satisfy – normally expressed in a temporal logic to express the expected dynamic aspects of the Model or in the form of an invariant that should be satisfied by all the states of the model. In this project we will focus our attention on the application of validation and verification techniques to the Model Driven Engineering of systems where resilience mechanisms are explicitly modelled and implemented according to that model.

Resilience corresponds to the fact that a system has the capability to adapt to harmful events and recover to a stable state or at least continue operation in a degraded mode without failing completely. These harmful events might cause the fundamental security properties (confidentiality, Integrity and availability) to be violated. With this project we aim at improving the state of the art of the construction of reliable resilient systems by using verification and validation techniques within the context of Model Driven Development (MDD).

The current trend of Software Engineering is to increasingly reason about the system being built at the model level by using appropriate Domain Specific Languages (DSL) for each conceptual domain. In this project we will concentrate on resilience and materialize it as a DSL. Model composition techniques can then be used in order to compose resilience features expressed in the resilience DSL with other domains equally defined as DSLs. When the composed model is validated, verification techniques can then be used to insure the resilience properties are well implemented. We will tackle this problem both at a theoretical and a practical level.

Contact: Nicolas Guelfi