Satellite event of Grace International Symposium on Advanced Software Engineering 2010

Mars 15th-17th 2010, Tokyo, Japan

Presentation

L’objectif de ce Workshop consiste à présenter les méthodes formelles B et B événementiel en tant que technique pour la spécification, la conception, le codage et la validation de logiciels basés sur des systèmes.

Supportée par les deux principales plateformes open source de modélisation (Rodin et l’Atelier B), la méthode formelle B est de plus en plus utilisée dans le cadre du développement d’applications industrielles dans le secteur ferroviaire et dans les domaines des cartes à puce. Ce Workshop a pour objectif de présenter les enjeux de B et du B événementiel dans leur état actuel de développement et d’exploitation, en mettant l’accent sur les outils supportant ces langages. Ce Workshop se compose de nombreuses présentations qui sont présentées par les membres du projet DEPLOY.

Le public attendu lors de cet événement concerne principalement des ingénieurs systèmes et logiciels ainsi que des chefs de projets et chercheurs dans le domaine des méthodes formelles.

Programme

Découvrir le compte-rendu de l’événement

Session 1

• The Big Picture (T. Lecomte)
• System-level modeling with Event B (M. Butler)
• The Rodin platform (M. Butler)

Session 2

• Model checking and animation with ProB (M. Leuschel)
• UML-B (M. Butler)
• Code generation (T. Lecomte / A. Requet)
• Sequential code in C / Ada
• PLCs
• VHDL

Session 3

• Automatic refinement (A. Requet)
• Industrial applications
  • Automatic pilots (Siemens, Alstom): (T. Lecomte)
  • Validation of large scale railway models: (M. Leuschel)
  • Event-B in space (Space System Finland case study)
  • Smartcard (Memory Protection Unit from STMicroelectronics): (T. Lecomte)