La thématique « De la recherche à l'enseignement des méthodes formelles - la méthode B en particulier » est interessante de plusieurs points de vue.
L'industrie du logiciel et notament celui du logiciel utilisé dans des environnements critiques, bénéficie largement non seulement des avancées de la recherche dans le domaine des méthodes formelles mais également de leur enseignement qui assure la formation des ingénieurs qualifiés, employés à l'issue de leurs diplômes.

Les méthodes formelles sont celles qui sont basées sur des bases mathématiques et qui permettent de construire rigoureusement des logiciels que l'on peut prouver corrects par rapport à des besoins et des exigences exprimées sous forme de propriétés dans les phases initiales de la construction.

La méthode formelle B en particulier est une méthode utilisée dans l'industrie ferroviaire pour les logiciels de contrôle à différents niveaux (conduite sans pilote, freinage, détection d'obstacles, portes palières, etc). Avec la généralisation des systèmes embarqués notamment, le recours aux méthodes rigoureuses sinon formelles pour construire les logiciels est devenu une approche incontournable. Des progrès sont observés en ce qui concerne les recherches dans ce domaine ; la méthode B par exemple offre un environnemnt outillé permettant de construire correctement des programmes à partir de leurs spécifications. Il est enseigné dans quelques Universités. Il se pose la question des qualifications et donc de la formation des techniciens et des ingénieurs à ce type de méthodes dans l'industrie. Les universitaires font l'effort d'introduire non sans difficultés, les méthodes formelles dans les cursus d'enseignement. Le partage des expériences et des leçons devra permettre d'améliorer l'offre de formation et aussi les résultats de recherche. Notre colloque vise cet objectif croisé entre enseignement et recherche.

La thématique de la construction de logiciels sûrs est développée par l'équipe COLOSS du LINA ; l'équipe est organisatrise du colloque.