LAUSR

Architectural tactics enable stakeholders to achieve cyber-resilience requirements. They permit systems to react, resist, detect, and recover from cyber incidents. This paper presents an approach to generate source code for architectural tactics typically used in safety and mission-critical systems. Our approach extensively relies on the use of the Event-B formal method and the EventB2Java code generation plugin of the Rodin platform. It leverages the modeling of architectural tactics in the Event-B formal language and uses a set of EventB2Java transformation rules to generate certified code implementations for the said tactics. Since resilience requirements are statements about a system over time, and because of the fact that the Event-B language does not provide (native) support for the writing of temporal specifications, we have implemented a novel Linear Temporal Logic (LTL) extension for Event-B. We support several architectural tactics for availability, performance, and security. The generated code is certified in the following sense: discharging proof obligations in Rodin - the platform we use for writing the Event-B models - attests to the soundness of the architectural tactics modelled in Event-B, and the soundness of the translation encoded by the EventB2Java tool attests to the code correctness. Finally, we demonstrate the usability of our resilience validation approach with the aid of an Autonomous Vehicle System. It further helped us increase our confidence in the soundness of our Event-B LTL extension.