Model-Driven Validation and Verification of Resilient Software Systems1. Statement of the research questions and/or hypothesesVerification 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 casesthat will, on the one hand find faults in an implementation – also called in the test literatureSystem Under Test (SUT) – and on the other hand increase trust in the final product. Withvalidation we worry about understanding if the model we are using as reference forimplementation and for extracting test cases from is sound. Formal validation is often achievedby mechanically proving properties the model should satisfy. For example, dynamic propertiescould be expressed in a temporal logic and static properties on the system state could beexpressed using logical invariants and then verified on the system’s model. In this project wewill focus our attention on the application of validation and verification techniques to the ModelDriven Engineering of systems where resilience mechanisms are explicitly modelled andimplemented according to that model. Resilience corresponds to the fact that a system has thecapability to adapt to harmful events and recover to a stable state or at least continue operationin a degraded mode without failing completely. These harmful events might cause thefundamental 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 resilientsystems by using verification and validation techniques within the context of Model DrivenDevelopment (MDD). The current trend of Software Engineering is to increasingly reason aboutthe 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 andmaterialize it as a DSL. Model composition techniques can then be used in order to composeresilience features expressed in the resilience DSL with other domains equally defined asDSLs. When the composed model is validated, verification techniques can then be used toinsure the resilience properties are well implemented. We will tackle this problem both at atheoretical and a practical level.