La thématique « De la recherche à l'enseignement des méthodes formelles - la méthode B en particulier » est intéressante de plusieurs points de vue. Les méthodes formelles en général constituent la seule façon de garantir la correction par construction des logiciels ; la méthode en particulier offre un cadre pratique en plein essor et déjà adopté par de nombreux industriels (Consortium européen Deploy par exemple).

L'industrie du logiciel et notamment celui du logiciel pour les 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 s'appuient 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 environnement outillé permettant de construire correctement des programmes à partir de leurs spécifications. Elle est enseignée 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.

Ce colloque international vise cet objectif croisé entre enseignement et recherche ; les deux dernières éditions ont montré l'intérêt de la communauté sur ce sujet. De plus, la thématique de la construction de logiciels sûrs est développée par l'équipe COLOSS de l'axe Architecture logicielle distribuée du laboratoire LINA ; l'équipe est organisatrice du colloque ; elle est impliquée dans les enseignements de génie logiciel et dans la formation au niveau Master, profil maintenant très recherché par des entreprises comme Systerel, Esterel Tech., Airbus, ClearSy, ....