Dr Sadegh Dalvandi

Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalability, we also require modular techniques with verifiable library abstractions. We address this challenge in the context of RC11 RAR, a subset of the C11 memory model that admits relaxed and release acquire accesses, but disallows, so-called, load-buffering cycles. We develop a simple framework for specifying abstract objects that precisely characterises the observability guarantees of abstract method calls. Our framework is integrated with an operational semantics that enables verification of client programs that execute abstract method calls from a library it uses. We implement such abstractions in RC11 RAR by developing a (contextual) refinement framework for abstract objects. Our framework has been mechanised inIsabelle/HOL

Cross-layer runtime management (RTM) frameworks for embedded systems provide a set of standard APIs for communication between different system layers (i.e. RTM, applications and device) and simplify the development process by abstracting these layers. Integration of independently developed components of the system is an error-prone process that requires careful verification. In this paper, we propose a formal approach to integration testing through automatic generation of runtime assertions in order to test the implementation of the APIs. Our approach involves a formal model of the APIs, developed using the Event-B formal method which is automatically translated to a set of assertions and embedded in the existing implementation of APIs. The embedded assertions are used at runtime to check the correctness of the integration. This work was supported by the EPSRC PRiME Project (EP/K034448/1), www.prime-project.org.

We demonstrate refinement-based formal development of the hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the Virtual Block Detector component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the Hybrid ERTMS Level 3 (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification’s state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.

The guarded atomic action model of Event-B allows it to be applied to a range of systems including sequential, concurrent and distributed systems. However, the lack of explicit sequential structures in Event-B makes the task of sequential code generation difficult. Scheduled Event-B (SEB) is an extension of Event-B that augments models with control structures, supporting incremental introduction of control structures in refinement steps. SEB-CG is a tool for automatic code generation from SEB to executable code in a target language. The tool provides facilities for derivation of algorithmic structure of programs through refinement. The flexible and configurable design of the tool allows it to target various programming languages. The tool benefits from xText technology for a user-friendly text editor together with the proving facilities of Rodin platform for formal analysis of the algorithmic structure.

This paper introduces a technique for modelling and verifying weak memory C11 programs in the Event-B framework. We build on a recently developed operational semantics for the RAR fragment of C11, which we use as a top-level abstraction. In our technique, a concrete C11 program can be modelled by refining this abstract model of the semantics. Program structures and individual operations are then introduced in the refined machine and can be checked and verified using available Event-B provers and model checkers. The paper also discusses how ProB model checker can be used to validate the Event-B model of C11 programs. We applied our technique to the C11 implementation of Peterson’s algorithm, where we discovered that the standard invariant used to characterise mutual exclusion is inadaquate. We therefore propose and verify new invariants necessary for characterising mutual exclusion in a weak memory setting.