Industrial uses of Formal Methods, B and ProB

Séminaire d'informatique
  • Quand ? 29/03/2018 à partir de 13:30 (America/Montreal / UTC-400)
  • Où ? Au local D4-2011 de la Faculté des sciences
  • Nom du contact
  • Participants Conférencier : Pr Dr Michael Leuschel, Heinrich Heine University Düsseldorf
  • Ajouter l'événement au calendrier iCal

Résumé: The B method is quite popular for developing provably correct software for safety critical railway systems, particularly for driverless trains. In recent years, the B method has also been used successfully for data validation (http://www.data-validation.fr). There, the B language has proven to be a compact way to express complex validation rules, and tools such as predicateB, Ovado or ProB can be used to provide high assurance validation engines, where a secondary toolchain validates the result of the primary toolchain.

This talk will give an overview of our experience in using formal methods in general and B in particular for industrial applications. We will also touch subjects such as training and readability. We will examine which features of B make it well suited for, e.g., the railway domain, but also point out some weaknesses and suggestions for future developments. We will also touch upon other formal methods such as Alloy or TLA+, as well as an overview of recent developments of ProB, useful for targeting new applications or formal languages (such as ASTDs). Of interest are maybe various new backends for model checking (TLC-backend and LTSMin integration) or constraint solving backends (SAT via Kodkod/Alloy and SMT via Z3 and CVC4) or the improved Java API allowing to deliver formal models as runtime-artifacts (executable models in the loop). This last part of the talk will be more informal and interactive, taking into account the interests of the audience.

La conférence sera donnée en anglais; les participants pourront interagir avec le conférencier en français s'ils le désirent.

 Toutes les personnes intéressées sont cordialement invitées.