Inférence de spécifications d'interaction avec stratégie adversariale

Les systèmes logiciels sont souvent développés de manière modulaire en (ré)utilisant des composants qui coopèrent pour fournir un service plus global. Nous considérerons les systèmes logiciels à base composants répartis, notamment ceux composés de composants communicants via le passage de messages et les primitives de communication. Des exemples de tels systèmes sont les systèmes client/serveur, les systèmes de contrôle des transports, l'Internet des objets, les véhicules autonomes connectés, etc. En pratique, l'assemblage de ces composants suit des procédures ad-hoc peu documentées. Par conséquent, la découverte de leurs spécifications formelles, c'est-à-dire l'inférence de spécifications [1,2], est d'un grand intérêt pour de nombreuses activités de vérification et de validation (V&V) de logiciels. Dans notre contexte, l'exploration exploitera les informations contenues dans les logs d'exécution des composants communicants. Ces logs sont souvent collectés via l'instrumentation ou le sniffing du code ou via une architecture de test. L'objectif du travail de doctorat est de développer de nouvelles méthodes d'inférence de spécifications d'interaction, telles que les modèles de diagrammes de séquence UML ou les Message Sequence Charts (MSC). Le cadre d'inférence sera fondé sur des travaux théoriques récents et outillage basés sur une sémantique opérationnelle de réécriture des modèles d'interaction développés conjointement par le CEA LIST et CentraleSupélec [4,5]. Il s'appuiera sur la génération de tests, guidée par des propriétés clés d'atteignabilité ou, plus généralement, des propriétés LTL (Linear Temporal Logic) qui exercent les composants contre des entrées de test peu communes, assurant ainsi une diversité dans leurs exécutions dans l'objectif de renforcer le processus d'inférence [3]. Le travail de doctorat sera lié au projet SELFY d'HORIZON Europe. N.B., SELFY signifie SELF assessment, protection & healing tools for a trustworthY and resilient CCAM, CCAM signifiant Cooperative, Connected and Automated Mobility. Le projet SELFY vise à accroître la sûreté, la sécurité, la robustesse et la résilience de l'écosystème CCAM par le développement d'une boîte à outils innovante composée d'outils collaboratifs, dont un outil de V&V basé sur l'inférence des spécifications d'interaction. Le doctorant sera impliqué dans une collaboration de recherche avec l'Université d'Okayama (Japon), un partenaire international associé au CEA dans le projet. [2] Sara Belluccini, Rocco De Nicola, Barbara Re, and Francesco Tiezzi. PALM: A technique for process algebraic specification mining. In Brijesh Dongol and Elena Troubitsyna, editors, Integrated Formal Methods ? 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings, volume 12546 of Lecture Notes in Computer Science, pages 397?418. Springer, 2020. [3] Hong Jin Kang and David Lo. Adversarial specification mining. ACM Trans. Softw. Eng. Methodol., 30(2):16:1?16:40, 2021. [4] Erwan Mahe. An operational semantics of interactions for verifying partially observed executions of distributed systems. (Sémantique opérationnelle des interactions pour la vérification d'exécutions partiellement observées de systèmes distribués). PhD thesis, University of Paris-Saclay, France, 2021. [5] Erwan Mahe, Boutheina Bannour, Christophe Gaston, Arnault Lapitre, and Pascale Le Gall. A small-step approach to multi-trace checking against interactions. In Chih-Cheng Hung, Jiman Hong, Alessio Bechini, and Eunjee Song, editors, SAC '21: The 36th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, Republic of Korea, March 22-26, 2021, pages 1815?1822. ACM, 2021.