Architectural Formal Modelling, Analysis & Synthesis

Summary
Detailed report on formalization of SerIoT architectural models, including behavioural models, security policy architectures for SerIoT use cases, and global security and safety properties. In addition, the report includes a methodology and proposed tool chain for automated security verification and for synthesizing run-time monitors from security policy architectures. The final M36 version includes an evaluation of the proposed security and safety verification tool chain applied to SerIoT use cases. This deliverable aims to be periodically updated throughout the project's lifetime. In particular, the initial version of this deliverable is foreseen to be produced in M12 while an updated version will follow in M24.