Publié le 10/01/2010 |

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

TimeTitleName
09:30 – 10:00Welcome, presentation of Rodin Platform 2.0Thierry Lecomte (CLEARSY)
10:00 – 10:45Modelling in UML-BColin Snook (University of Southampton, UK)
11:00 – 11:45Refinement in UML-BColin Snook (University of Southampton, UK)
11:45 – 12:30ProB for Animation, Model Checking and Constraint SolvingMichael Leuschel (University of Dusseldorf)
14:00 – 15:00Potpourri of what ? One year in a DA’s lifeAryldo G. Russo Jr. (Aes)
15:00 – 15:30Deployment in business information softwareAndreas Roth (SAP, Germany), Thierry Lecomte (CLEARSY, France)
16:00 – 16:45Validation of Railway Properties with ProBMichael Leuschel (University of Dusseldorf)
16:45 – 17:30Evaluating a control system architecture based on a formally derived AOCS modelDubravka Ilic (Space Systems Finland)

Jour 2

TimeTitleName
09:30 – 10:00Proving Reachability in B using Substitution RefinementMarc Frappier, Amel Mammar and Fama Diagne
10:00 – 10:45A Proof-Based Approach to Verifying Reachability PropertiesMarc Frappier, Amel Mammar and Fama Diagne
11:00 – 11:45Integrating Rodin with SMT-SolversVítor Alcântara and David Déharbe
11:45 – 12:15B for RealThierry Lecomte (CLEARSY)
14:00 – 15:00Modularisation in Event-BAlexei Iliasov (Newcastle University, UK)
15:00 – 15:45A Methodological WRSPM Approach to a B Formalization in an Industrial SettingHaniel Barbosa, Aryldo G. Russo Jr., and David Déharbe
16:00 – 16:45From system to softwareThierry Lecomte (CLEARSY)
16:45 – 17:00Questions, 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:

Historique

De nombreuses journées dédiées à la dissémination de B ont été organisées depuis les 6 dernières années :