8-9 Novembre 2010, Natal, Brésil
Présentation
Ce workshop B/event-B est organisé dans le cadre du projet DEPLOY. Il a pour objectif de présenter l’état d’avancement des travaux de recherche et de développement autour des langages B et Event-B, ainsi que les applications en vraie grandeur à des problématiques industrielles. Les sujets abordés lors de ce workshop sont nombreux et incluent notamment :
- Développement d’outils (extensions du langage, démonstrateurs tiers, génération de code, etc.)
- Techniques de modélisation (propriétés temps-réel, raffinement probabiliste, patrons de conception, logique d’ordre supérieur, etc.)
- Déploiement (méthodologie, cas d’études, retour d’expérience, passage à l’échelle, etc.)
Les chercheurs sont invites à contribuer au programme de la seconde journée au travers d’un appel à article ouvert.
Programme
Le workshop dure 2 jours :
- Le premier jour est réservé aux orateurs du projet DEPLOY. La présentation générale du projet et des outils sera accompagnée de présentations ciblant des sujets techniques et scientifiques (modélisation du temps, génération de code, animation de modèles, model checking, etc.) faisant l’objet de travaux dans le cadre du projet DEPLOY. Le témoignage d’industriels des domaines de l’espace, des systèmes d’information, du transport ferré et de l’automobile complétera la journée.
- Le second jour est ouvert à tout orateur, au travers d’un appel à contribution à paraître. Un large spectre d’article est attendu, allant des travaux théoriques jusqu’aux applications pratiques de B/event-B. La sélection des articles sera fera au travers d’un comité de programme.
Programme
Jour 1
| Time | Title | Name |
|---|---|---|
| 09:30 – 10:00 | Welcome, presentation of Rodin Platform 2.0 | Thierry Lecomte (CLEARSY) |
| 10:00 – 10:45 | Modelling in UML-B | Colin Snook (University of Southampton, UK) |
| 11:00 – 11:45 | Refinement in UML-B | Colin Snook (University of Southampton, UK) |
| 11:45 – 12:30 | ProB for Animation, Model Checking and Constraint Solving | Michael Leuschel (University of Dusseldorf) |
| 14:00 – 15:00 | Potpourri of what ? One year in a DA’s life | Aryldo G. Russo Jr. (Aes) |
| 15:00 – 15:30 | Deployment in business information software | Andreas Roth (SAP, Germany), Thierry Lecomte (CLEARSY, France) |
| 16:00 – 16:45 | Validation of Railway Properties with ProB | Michael Leuschel (University of Dusseldorf) |
| 16:45 – 17:30 | Evaluating a control system architecture based on a formally derived AOCS model | Dubravka Ilic (Space Systems Finland) |
Jour 2
| Time | Title | Name |
|---|---|---|
| 09:30 – 10:00 | Proving Reachability in B using Substitution Refinement | Marc Frappier, Amel Mammar and Fama Diagne |
| 10:00 – 10:45 | A Proof-Based Approach to Verifying Reachability Properties | Marc Frappier, Amel Mammar and Fama Diagne |
| 11:00 – 11:45 | Integrating Rodin with SMT-Solvers | Vítor Alcântara and David Déharbe |
| 11:45 – 12:15 | B for Real | Thierry Lecomte (CLEARSY) |
| 14:00 – 15:00 | Modularisation in Event-B | Alexei Iliasov (Newcastle University, UK) |
| 15:00 – 15:45 | A Methodological WRSPM Approach to a B Formalization in an Industrial Setting | Haniel Barbosa, Aryldo G. Russo Jr., and David Déharbe |
| 16:00 – 16:45 | From system to software | Thierry Lecomte (CLEARSY) |
| 16:45 – 17:00 | Questions, End of the workshop |
Le workshop aura lieu les deux jours précédant la conférence, sur le site de celle-ci Imira Plaza.
Responsable du workshop:
- Thierry Lecomte (CLEARSY)
Historique
De nombreuses journées dédiées à la dissémination de B ont été organisées depuis les 6 dernières années :
- Rodin Industry Day (Avril 2006, Aix en Provence, France)
- Rodin Industry Day (Septembre 2007, Paris, France)
- B Dissemination Day (Août 2008, Salvador de Bahia)
- B Dissemination Day (Août 2008, Sao Paulo, Brésil)
- Recent Innovations and Applications in B (Novembre 2009, Eindhoven, The Netherlands)
- B Dissemination Day (Mars 2010, Tokyo, Japon)