DS0704 - Sciences et technologies logicielles

Méthode outillée de modélisation formelle des exigences pour des systèmes complexes critiques – FORMOSE

Résumé de soumission

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.

Coordinateur du projet

Madame Régine Laleau (Université Paris-Est Créteil Val de Marne - Laboratoire d'Algorithmique, Complexité et Logique)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

Thales Thales
UPEC/LACL Université Paris-Est Créteil Val de Marne - Laboratoire d'Algorithmique, Complexité et Logique
IMT TB Institut Mines Telecom
CLEARSY

Aide de l'ANR 788 526 euros
Début et durée du projet scientifique : septembre 2014 - 48 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter