Projet ANR-14-CE28-0009 – FORMOSE : Méthode outillée de modélisation formelle des exigences pour des systèmes complexes critiques
Programme : Sciences et technologies logicielles (DS0704) 2014
Année de financement : 2014
Coordinateur du projet : Madame Régine LALEAU (Université Paris-Est Créteil Val de Marne - Laboratoire d'Algorithmique, Complexité et Logique)
Partenaires : PME; Institut Mines-Télécom; THALES; Laboratoire public
Montant : 788526.0 euros
Date de début : 2014
Durée : 60 mois
Résumé : Le projet Formose est un projet de recherche industrielle dont l'objectif est de produire une méthode formelle d'ingénierie des exigences (IE) orientée modèles pour des systèmes complexes critiques, supportée par un outil libre. C'est un projet de 48 mois auquel participent 2 partenaires académiques (LACL – porteur du projet –, Institut Mines-Telecom) et deux partenaires industriels (THALES, ClearSy).
L'IE est un processus critique dans la conception de logiciels et de systèmes. Une part importante des coûts de développement logiciel ou système est d’ailleurs imputable à la compréhension du domaine et des exigences. Cependant, les pratiques industrielles actuelles ne sont pas assez efficaces. Elles consistent principalement en processus « maison », retour d’expérience et outils de gestion des exigences (macros dans des outils de traitement de texte, outils de « traçabilité » et base de données d’exigences). Même si ces dernières années de nombreux projets de recherche ont produit des avancées notables et ont atteint un niveau de maturité suffisant, des études récentes ont montré que des problèmes persistent. Le projet Formose vise à résoudre plusieurs défis soulevés par ces problèmes, en particulier les plus cruciaux pour les systèmes complexes critiques. Ils concernent la nécessité de prendre en compte la grande complexité de ces systèmes, d'une meilleure intégration de l'IE avec les techniques de vérification et de validation pour assurer une meilleure qualité des exigences, et plus généralement d'un guide méthodologique et d'un support outillé pour accompagner le processus de construction de modèles des exigences. Les principaux résultats du projet seront les suivants. Tout d'abord, nous définirons un langage de modélisation des exigences intégrant les concepts de base de langages existants comme KAOS ou Tropos/i*, tout en ajoutant de nouveaux concepts pour tenir compte des caractéristiques propres des systèmes complexes critiques : leur architecture abstraite sera considérée en permettant la modélisation des exigences à plusieurs niveaux d'abstraction tout en assurant leur cohérence; le langage permettra de spécifier les exigences non fonctionnelles de sûreté et de performance mais aussi les exigences induites par l'existence de différents modes opératoires et de reconfigurations. Le langage sera multi vues (langage naturel, notations graphiques et formelles), pour être compréhensible par toutes les parties prenantes. Pour l'aspect vérification, nous utiliserons des méthodes formelles complémentaires existantes, supportées par des outils efficaces : la méthode B et le model-checker temporisé UPPAAL. Puis nous définirons un processus personnalisable pour guider les ingénieurs dans leurs différentes activités de construction d'un modèle des exigences. Nous utiliserons la plate-forme OpenFlexo pour supporter la mise en oeuvre de ce processus. Elle intègrera les outils ad hoc développés dans le projet et les outils de vérification existants. Elle sera capable d'envoyer des obligations de preuve aux prouveurs, de recevoir la réponse de ces prouveurs et de les interpréter pour les présenter aux utilisateurs en utilisant les représentations adéquates. Enfin, pour s’assurer de la pertinence des résultats, la méthode et les outils seront évaluées tout au long du projet sur les études de cas fournies par les partenaires industriels. De plus, les ingénieurs de THALES et ClearSy seront des utilisateurs actifs de la méthode et des outils pour donner des retours réels sur leur utilisabilité. Clearsy assurera l'exploitation et la maintenance des outils après la fin du projet et THALES développera la version industrielle des outils.
La dissémination des résultats sera assurée par un site web, des publications dans des revues et conférences internationales et nationales, ainsi que la disponibilité gratuite de la plate-forme. Nous envisageons également de communiquer avec la communauté industrielle du domaine des systèmes complexes critiques.