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