UMLB :

Orateur: Colin Snook
Description:   UML-B provides a UML-like graphical front-end for Event-B modelling. It adds class oriented and state machine modelling capabilities. UML-B is automatically translated into Event-B for analysis and verification.

Mobility

Orateur: Apostolos Niaouris

Description: The mobility plug-in is a tool that can be used for the automatic verification of mobile agent systems. For the specification of such systems, we are using a newly developed high level programming notation. This language is a hybrid of Event-B combined with constructs inspired by two process algebras (KLAIM and pi-calculus) and is capable of capturing both the functional and behavioural models of agents. Furthermore, the tool is capable of model checking Event-B specifications (deadlock detection and invariants checks). The model checking engine is based on Petri nets unfoldings.

ProB

Orateur: Michael Leuschel 

Description: The ProB Plug-In for Rodin is capable to automatically animate EventB models  and can be used to systematically check a model for errors. In addition it can assist the proving process and can be used as a disprover on individual proof obligations.

Brama

Orateur: Antoine REQUET 

Description: Brama enables animating B models within Rodin Platform. Animation capabilities are twofold: first, debugging B models: the design can verify by experiment that a model and a system have similar behaviour. Second, connecting B models with flash animation: B models are used to trigger flash animation.

From Grafcet to B : An experiment (with mixed results)

Orateur: Sébastien Loison (RATP), Louis Mussat (ClearSy) 
Description : This experiment consisted in modeling with the event-B formalism a tiny part (namely two automata) of a software-based train system. Translating from the GRAFCET-like specification of the automata was nearly straightforward, but it was nearly impossible to retrieve enough high-level information to be able to prove some useful properties.

Validation of Microkernel - Based Systems B Models with Brama

Orateur: Sophie Gabrielle (STMicroelectronics), Julien Millot (ClearSy)
Description : A Microkernel-based API has been modeled in order to formally prove security properties such a memory isolation or application communication restrictions. Proof obligations shows that the B model is coherent in term of security, but don't show the system's availability required for a real use. Brama by animating such API models allows to create the full data structure and to validate the model in term of concurrent access behaviour.

Towards the Formal Verification of a Java Processor in Event-B

Orateur: Neil Evans 
Description : We present an initial attempt to model and verify an (almost complete) implementation of a Java Virtual Machine in hardware. We show that verification of the processor's microcoded architecture can be achieved using Event-B refinement.

Modéliser la commande de portes palières

Orateur: Florent Patin (ClearSy)
Description : We present some recent applications of the B formal method to the development of safety critical systems, namely platform screen door controllers. These SIL3/SIL4 compliant systems have their functional specification based on a closed formal model. This model has been proved, guaranteeing a correct by construction behaviour of the system in absence of failure of its components. The constructive process used during system specification and design leads to a high quality system which has been qualified by French authorities. 

Modelling an Interlocking System with the Rodin Platform

Orateur: Christophe Métayer (Systérel), Laurent Voisin 
Abstract : The main requirement on an interlocking system is to prevent train collisions, through a computer-based controller that manages points and signals. We present here how such a system can be modelled using the Rodin platform and proved to fulfil its requirements. We will also show how the system model allows to discover hidden assumptions on the system.