Research and development of CITADEL project technologies will continue through May 2019. Many deliverables are confidential due to the sensitivities related to protecting Europe's Critical Infrastructures, however the following public results developed during the first half of the project are available for download:
CITADEL Modeling and Specification Languages
This report proposes a new modeling language suitable to describe a dynamic system architecture. The language has a formal semantics to enable verification with formal methods. It supports the design of the communication among components and the monitoring of failures. Finally, it comes with a property specification language to formalize the system properties that must be ensured by the system architecture and protected from component failures such as malfunctioning or disruption of the communication network.
Interfaces and workflow definition for Adaptive-MILS Evidential Tool Bus
This report proposes a preliminary design of the Adaptive-MILS Evidential Tool Bus (AM-ETB) and interfaces for integration within the CITADEL proposed workflow. The primary objective of AM-ETB is to enable the timely re-construction of assurance cases for Adaptive-MILS systems along their evolution, and therefore to support a dynamic re-evaluation and/or re-certification process. In the proposed design, AM-ETB coordinates the construction of an assurance case by using (1) assurance case patterns, that is, generic arguments and reasoning schemes for Adaptive-MILS, (2) up-to-date system models and properties, that is, faithful abstractions of the system configuration and functionality and (3) machineable evidence, that is, automatically checkable analysis and validation results obtained using dedicated tools on system models.
Methodology for Industrial Evaluation and Readiness Assessment
This report presents the methodology to monitor and evaluate the achievement of the CITADEL project objectives, by means of the three industrial demonstrators planned to be implemented in the project. In addition, it defines the means to verify that the CITADEL solutions implemented in each demonstrator meets preestablished operational objectives and levels of technological maturity.