RODIN INDUSTRY DAY
PROGRAMME DE LA JOURNEE - 10 septembre 2007 - Paris
Programme
Cette seconde journée industrielle conclut le projet Rodin et est l'occasion de présenter la plateforme de modélisation formelle RODIN, des plugins applicatifs qui étendent ses capacités, ainsi que des applications industrielles réalisées en dehors du projet RODIN.
La langue utilisée est l'anglais.
PROGRAMME
Matin: Présentation de la plateforme
 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
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.
|
|
Après midi : Utilisation Industrielle de 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
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.
|
|
E-mail : contact@clearsy.com
|
