Groupe de travail – Méthodes formelles

Objectif

Ce GT est consacré aux méthodes formelles de développement.
Il organise un cycle de conférence/forum pour présenter bien sûr les fondements théoriques de ces méthodes, mais surtout faire un état de l’art et de la pratique, démystifier, échanger, et pourquoi pas monter ensemble des projets pour “passer à l’acte” ?
Les intervenants y sont à la fois des scientifiques et universitaires les plus compétents dans ces domaines et des utilisateurs “de terrain” qui ont déjà pratiqué ces méthodes et livrent leurs retours d’expérience.

Contexte

Ces méthodes ne sont pas assez connues mais ont un potentiel énorme pour faire progresser la productivité ET la qualité intrinsèque des développements de logiciels embarqués et de leurs outils de développement et de vérification. Et elles ne sont pas si difficiles à mettre en œuvre.
La première édition du Forum Méthodes Formelles (FMF) a eu lieu à Toulouse fin 2012 à l’initiative du DAS SE2L du pôle Aerospace Valley et du thème IFSE du RTRA AESE . De nouveaux partenaires ont rejoint l’organisation du forum depuis : pôle Minalogic en 2013, labex Digicosme en 2014, pôle Systematic en 2015.
FMF est devenu un groupe de travail d’ Embedded France en 2015.

Plan de travail du GT et livrables

Deux sessions du forum sont organisées annuellement. Les conférences ont lieu à Toulouse au LAAS-CNRS et sont retransmises en direct à Grenoble au centre INRIA Rhone Alpes ainsi que sur le campus de Saclay.
Le GT enregistre les sessions des forums ; les présentations effectuées et les vidéos sont disponibles sur ce site web : http://projects.laas.fr/IFSE/FMF/

Actualités

Assises de l’Embarqué consacrées à la convergence sûreté/sécurité dans les Systèmes Embarqués – 19 novembre 2019, Bercy
A l’occasion de ces Assises le groupe « Méthodes formelles » et le groupe « Sûreté des STRC » (Systèmes temps réel et communicants) ont annoncé leur fusion. Ils donnent naissance au groupe ISEC

«ISEC, Ingénierie des Systèmes Embarqués Critiques sûrs». Ce groupe a pour but de capitaliser autour de l’Ingénierie Système par composition formelle intégrant la prise en compte de leur sûreté. La sûreté est prise dans son acceptation anglo-saxonne ”Dependability”; Elle englobe « Sûreté de Fonctionnement (SdF) et Cyber Sécurité (CS) ». Ce groupe s’intéresse à la Formalisation de la Sûreté des systèmes (FS), avec raffinement par machines à états, algèbre évolutive et “Machine Learning (ML)”.  L’objectif poursuivi est de Vérifier Formellement (VF) le maximum de propriétés, sur cas d’étude (CE), afin de permettre le déploiement d’architectures sûres pour ces systèmes.  Etablie lors de la réunion de lancement début 2020, la feuille de route aura pour objectif d’atteindre en régime de croisière des points d’avancement réguliers, à savoir : SdF (3) ; CS (3) ; « FS & VF » (2) ; CE (2). La périodicité des points par thématiques suivra le calendrier scolaire. 

Liste des membres

CEA, C&S – Systerel – Atos – INRIA – Aerospace Valley – Adacore – IRIT – LRI-Université Paris-Sud – Minalogic – LSV/CNRS – Airbus – LAAS/CNRS – ONERA