This paper presents the formal modelling and refinement of a chat system using the Event-B formal method. We elicit software requirements as User Stories and manually map them into Event-B . We model core chat functionalities, including user creation, chat session creation, message sending, message forwarding, and message deletion, while ensuring consistency via invariants and proof obligations in Rodin. We discuss challenges, lessons learnt, and propose several best modelling practices for the design and verification of similar event-driven messaging systems. Our work outlines directions for future integration with tool-supported code generation.

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 theEvent-Bformal method and theEventB2Javacode generation plugin of the Rodin platform. It leverages the modeling of architectural tactics in theEvent-Bformal language and uses a set ofEventB2Javatransformation 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 theEvent-Blanguage does not provide (native) support for the writing of temporal specifications, we have implemented a novel Linear Temporal Logic (LTL) extension forEvent-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 theEvent-Bmodels - attests to the soundness of the architectural tactics modelled inEvent-B, and the soundness of the translation encoded by theEventB2Javatool 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.

Most code generation tools for Event-B are designed for generating small, in-memory applications such as embedded controllers. In this work, we investigate whether the EventB2SQL tool (Wang and Wahls, LNCS 8702) can generate satisfactory code for the OpenBravo POS ERP (Enterprise Resource Planning) system by replacing the database core of the system with code generated from an Event-B model. We describe our methodology for generating code with EventB2SQL and enhancements to EventB2SQL that improve the performance of the generated code, and present empirical results and a user study comparing the performance of OpenBravo POS as is and with its core replaced by code generated by EventB2SQL.

A recent trend in object oriented programming languages is the use Access Permissions (AP) as abstraction to control concurrent executions. AP define a protocol specifying how different references can access the mutable state of objects. Although AP simplify the task of writing concurrent code, an unsystematic use of permissions in the program can lead to subtle problems. This paper presents a Linear Concurrent Constraint (lcc) approach to verify AP annotated programs. We model AP as constraints (i.e., formulas in logic) in an underlying constraint system, and we use entailment of constraints to faithfully model the flow of AP in the program. We verify relevant properties about programs by taking advantage of the declarative interpretation of lcc agents as formulas in linear logic. Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. We show that those properties are decidable and we present a complexity analysis of finding such proofs. We implemented our verification and analysis approach as the Alcove tool, which is available on-line.