About us
Espace utilisateur
Education
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Thesis
Home   /   Thesis   /   Interaction specification mining with adversarial examples

Interaction specification mining with adversarial examples

Abstract

Software systems are often developed in a modular way by (re)using components that cooperate in providing a more global service. We will consider component-intensive software systems, particularly those composed of communicating components via message passing and communication primitives. Examples of such systems are client/server systems, transportation control systems, Internet of Things, connected autonomous vehicles, etc. In practice, the assembly of these components follows poorly documented ad-hoc procedures. Therefore, discovering their formal specifications, i.e., specification mining [1,2] is of great interest for many software Verification and Validation activities (V&V). In our context, mining will exploit the information contained in the execution logs of the communicating components. These logs are often collected via code instrumentation or sniffing or via a testing architecture. The objective of the doctoral work is to develop new methods for mining interaction specifications, such as models of UML Sequence diagrams or Message Sequence Charts (MSC). The foreseen mining framework will be grounded by recent theoretical work and supporting tooling on operational rewriting semantics of interaction developed conjointly between CEA LIST and CentraleSupélec [4,5]. It will encompass test generation, guided by key reachability properties or, more generally, LTL (Linear Temporal Logic) properties that adversely exercise the components against uncommon test inputs and thus ensuring diversity in their executions for more efficient mining [3]. The doctoral work will be related to HORIZON Europe project SELFY. N.B., SELFY stands for SELF assessment, protection & healing tools for a trustworthY and resilient CCAM, CCAM stands for Cooperative, Connected and Automated Mobility. The project SELFY aims to increase the CCAM ecosystem’s safety, security, robustness, and resilience by researching and developing a toolbox made of collaborative tools, including a V&V tool based on interaction specification mining. The PhD student will be involved in research collaboration with Okayama University (Japan), an international associate partner linked to CEA in the project.

[1] Glenn Ammons, Rastislav Bodik, and James R. Larus. Mining specifications. In John Launchbury and John C. Mitchell, editors, Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002, pages 4–16. ACM, 2002.

[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.

Laboratory

Département Ingénierie Logiciels et Systèmes (LIST)
LSL (DILS)
Laboratoire pour la Sûreté du Logiciel
Top pencilenvelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down