L’équipe ARGOS (Advancing Rigorous Software and System Engineering) regroupe des compétences recouvrant le développement de logiciel tout au long de son cycle de vie, avec une souci particulier dans l’utilisation de techniques permettant le développement de systèmes et logiciels de qualité. Dans cette optique, l’équipe se propose de relever des défis autour de la correction des logiciels et des systèmes, du développement de systèmes sécurisés, ainsi que de l’adaptation et optimisation des processus et des conceptions.

Les problèmes traités par ces trois axes sont étudiés en utilisant des modèles et des patrons de conception, intégrant l’expression formelle des propriétés à vérifier. Une attention particulière est portée à la construction d’outils support des méthodes développées, sur la base des plates-formes outils existants (lien) et la réalisation d’évaluations et d’expérimentations des recherches menés.

Mots clés : génie logiciel, ingénierie système, spécification et vérification formelle, ingénierie à base de modèles, validation de modèles, ingénierie de langages, langages (de modélisation) dédiés, patrons & bonnes pratiques, méthodes agiles, gestion de processus, évaluation empirique

Sujets scientifiques liés : Conception et construction de systèmes

Domaines d’application : systèmes cyber-physiques, robotique, cloud

Correction des logiciels et des systèmes

L’enjeu scientifique de cet axe concerne la qualité des logiciels et des systèmes, du point de vue du respect des exigences fonctionnelles et non fonctionnelles. L’objectif des travaux de l’axe est de faciliter la construction correcte et la validation des logiciels et des systèmes en utilisant des approches rigoureuses de spécification et de vérification issues des méthodes formelles.

Nos travaux s’appuient sur différentes techniques de spécification formelle à base de modèles logiques ou opérationnels (logiques temporelles, automates, algèbres de processus), ainsi que sur différentes méthodes d’analyse de ces modèles (model-checking, interprétation abstraite, preuve, test). Raisonner en amont sur des modèles des systèmes à développer permet d’abstraire la complexité des systèmes et d’assurer que ces systèmes présentent les propriétés souhaitées.

Une attention particulière est portée à intégrer les techniques formelles dans le développement traditionnel en les rendant accessibles aux ingénieurs du terrain. Une spécificité de nos travaux est de mettre à contribution des techniques de l’ingénierie des modèles (IDM) ainsi que des langages de modélisation standards de l’industrie (e.g., UML, SysML). Nous nous intéressons à la sémantique de ces langages, à l’intégration de spécifications formelles, à l’application de méthodes de vérification, basées notamment sur le model-checking, ainsi qu’au test.

Développement rigoureux des architectures sécurisées

L’enjeu scientifique de cet axe est de répondre à la double nécessité de construire des systèmes résilients d’un point de vue cyber-sécurité, tout en garantissant leur richesse fonctionnelle.

Les activités de recherche visent le développement d’un cadre méthodologique de conception permettant de gérer et d’intégrer à la fois les éléments garants de la sécurité du système et l’architecture de la chaîne fonctionnelle, tout en assurant une validation continue de la sécurité et de l’architecture.

Le but ultime est de bâtir de nouvelles pratiques visant à accroître la réutilisation de patrons de conception sécurisée pour réduire les coût des développements tout en augmentant la confiance dans les systèmes.

Adaptation et optimisation des processus et des conceptions

L’enjeu scientifique est l’accompagnement de l’émergence de nouveaux processus et de nouvelles architectures répondant aux besoins d’adaptation au changement.

Au niveau processus, nous cherchons à contrôler les activités de développement pour assurer leur cohérence et la traçabilité. Puis nous visons à appliquer des pratiques et techniques pour rendre le développement plus flexible et adaptatif afin d’améliorer en permanence les processus de développement. Nous nous intéressons à l’encadrement de l’émergence de processus de développement spécifiques élaborés par les équipes agiles et à des langages de patterns pérennisant les conceptions émergentes issues de ces approches. Nous travaillons également sur l’optimisation de la représentation des modèles pour aller vers des Systèmes de Gestions de Bases de Modèles.