Publié le 10/01/2010 |

Satellite event of SBMF 2010

November 8th-9th 2010, Natal, Brazil


This B / event-B workshop is organized on behalf of the DEPLOY project. Its objectives are to present current status and ongoing research and development related to B and event B languages and tools, as well as applications to industry size problems. Topics addressed by the workshop are many, including but not limited to:

  • Tool development (language extensions, external provers, code generation, etc.)
  • Modelling challenges (real time properties, probabilistic refinement, design patterns, high order logic, etc.)
  • Deployment (methodology, cases-studies, return of experience, scaling up, etc.)
  • Teaching and training

Researchers are invited to contribute to the second day of the workshop through an open call for papers.


The workshop lasts 2 days:

  • The first day is devoted to DEPLOY speakers. General presentation of the project and tools will be sided by focused talks on scientific/technical matters (modelling time, code generation, model animation, model checking, etc.) that are being researched in DEPLOY. Reports on industrial applications (space, railways, automotive, information systems, etc.) will complete the day.
  • The second day is open to any presenter, through an international call for papers. Expected contributions would range from theoretical research to practical applications of B/event B. Submissions are handled by the programme committee.

Day 1

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)

Day 2

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

The workshop is collocated with the SBMF conference (Monday and Tuesday), at the Imira Plaza hotel.

Workshop Chair:


Several B dissemination days have been organized over the last 6 years:

  • Rodin Industry Day (April 2006, Aix en Provence, France)
  • Rodin Industry Day (September 2007, Paris, France)
  • B Dissemination Day (August 2008, Salvador de Bahia)
  • B Dissemination Day (August 2008, Sao Paulo, Brazil)
  • Recent Innovations and Applications in B (November 2009, Eindhoven, The Netherlands)
  • B Dissemination Day (March 2010, Tokyo, Japan)