Home l News l Company l Activities l Sectors l Sale Assistance l Our Projects l Conferences
Our Products and Training l Our Values l Employment l Newsletter l Contacts l Site Map    -  

RODIN INDUSTRY DAY

DAY’S PROGRAM - 10 september 2007 - Paris

Program

This second industrial day concludes the Rodin project and provides an opportunity to present the formal Rodin modelling platform, some applicable plug-ins which broaden its capabilities, as well as some industrial applications achieved outside the RODIN project.

The language used is English.

 PROGRAM

Morning : Welcome Coffee (9h30 - 10h00)

Morning : Presentation of the platform (10h00 - 12h30)
Introduction to Rodin

Alexander Romanovski

Rodin Methods to develop fault tolerant systems Elena Troubitsyna

Rodin platform Jean Raymond Abrial

Rodin platform demonstration Jean Raymond Abrial

Introduction to Rodin plug-ins Michael Butler

      UMLB

 Colin Snook  
      Mobility

Apostolos Niaouris

      Pro B

Michael Leuschel 

      Brama

Antoine REQUET 

Lunch : Free buffet (12h30 - 14h00)
Afternoon : Industrial use of Rodin (14h00 - 17h00)
From Grafcet to B : An experiment (with mixed results)

Sébastien Loison (RATP),
Louis Mussat (ClearSy)

Validation of Microkernel - Based Systems B Models with Brama

Sophie Gabrielle (STMicroelectronics)
Julien Millot (ClearSy)

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

Neil Evans
(Atomic Weapons Establishement)

Modeling Platform Screen Doors Systems

Florent Patin (ClearSy)

Modeling an Interlocking System with the Rodin Platform

Christophe Métayer (Systérel)
Laurent Voisin

 

Morning: Presentation.

UMLB :

Speaker: 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

Speaker: 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

Speaker: 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

Speaker: 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.

 

Afternoon: Industrial Use of Rodin

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

Speaker : 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.

  
   

Modelling Platform Screen Doors Systems

Speaker: 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

Speaker: 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.

 

E-mail : contact@clearsy.com