Model-Driven Validation and Verification of Resilient Software Systems - MOVERE

Coordinating Institution: Université du Luxembourg
Contracting Partner(s): University of Geneva (CH)
From: 01/05/2010
To: 30/04/2013
Budget: 265,000.00€
Contact(s): Guelfi Nicolas

Summary

Verification and Validation of software have nowadays clear meanings in the context of Model-Driven Development. With test based verification we worry about producing a set of test cases that will, on the one hand find faults in an implementation – also called in the test littérature System Under Test (SUT) – and on the other hand increase trust in the final product. With validation we worry about understanding if the model we are using as reference for implementation and for extracting test cases from is sound.

Formal validation is often achieved by mechanically proving properties the model should satisfy. For example, dynamic properties could be expressed in a temporal logic and static properties on the system state could be expressed using logical invariants and then verified on the system’s 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 opération 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 résilient 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.