Thomas Fayolle

Doctorant en cototutelle :
LACL - Université de Paris Est Créteil - FRANCE - mail : tfayolle[at]lacl.fr
GRIL - Université de Sherbrooke - QUÉBEC (CANADA) - mail : thomas.fayolle@usherbrooke.ca

Sujet : Combinaison de méthodes formelles pour la spécification de systèmes ferroviaires
Subject : Combining formal methods to specify train systems

Reports

  • Specifying a Train System using ASTD and the B method
    You can download the associated files here

    • ABZ Case study

  • This files present an answer to the ABZ case study

  • Proof of ASTD to B translation using Coq

  • An implementation of the translation of a subset of the ASTD language into B have been written and proven using the Coq Proof Assitant. The Coq files are here. A quick explanation of the files can be seen here.