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.