Join CEA to Add Meaning to Your Work, Lead and Support National and International R&D Projects, Nurture and Ignite Your Curiosity.

IN SUMMARY, WHAT DO WE OFFER YOU?
Runtime Verification (RV) is at the crossroads of formal verification and monitoring. It consists in analyzing system executions, as observed by means of a monitoring
architecture, in order to verify their conformity to a formal reference model, characterizing the set of acceptable behaviors of the system. When dealing with distributed systems, the ability of an RV technique to analyze the communication flows between the subsystems is a central element, since distributed systems are composed of subsystems deployed on different machines and interacting by message passing to perform services. This ability relies first on the expressivity of the language used to
specify the formal reference models. It is essentially a question of being able to model asynchronous communications between concurrent processes. This is possible in a wide variety of formalisms, including formalisms derived from Message Sequence Charts (MSC) and UML sequence diagrams (UML-SD). We refer to such models as "interactions".
CEA LIST is developing the MAAT IAT (Interaction Analysis Tool) to analyze distributed system executions and confront them with interactions. When the system is running, execution traces are logged on each of the subsystems. The traces of all the subsystems are gathered in a trace tuple, which is then analyzed by an RV algorithm.

The principles of this approach are detailed in several publications [1,2].
There are two types of RV approaches: offline and online approaches. In offline approaches, the observed executions are collected a priori during a logging phase, while in online approaches, the verification process continuously interacts with the monitoring architecture.

YOUR MISSION:
The preciseness of the information computed by an RV algorithm depends on how precise the observations of the system executions are. When dealing with online runtime verification such observations are realized via a so-called monitoring architecture. The monitoring architecture should be reliable, that is avoid losing information, and rapid enough to allow the RV algorithm to perform its analysis as soon as possible, trying to cope with the frequency of observations imposed by the system execution. One of the practical limitations of online RV is that, for economic reasons, it is often not possible to design and implement a complete monitoring architecture from scratch, for each new system to be verified. It is therefore desirable to design a generic library of monitoring functionalities that can be used for that purpose. You will contribute to the design and implementation of such a library for the MAAT IAT tool.

DO YOU STILL HAVE A DOUBT?

The sidelines of your main mission may interest you:

• Acutting-edge research ecosystem, unique in its kind and dedicated to themes of high societal importance, which gives meaning to your mission
• Trainingto strengthen your skills, acquire new ones and boost your mission
• A work/life balance recognized by our employees
• The possibility ofteleworkingto balance transport times and contribute to your quality of life
• Aworkscouncilrich in benefits and social, cultural and sporting activities
• A workplace in the heart of adynamicplateau, surrounded by schools andtech companies
• A subsidizedcompany restaurantnearby
• Acompany savings planwith employer contribution
• Public transportcosts coveredat 75%
• Dedicatedshuttlesfrom Paris

REQUIRED SKILLS :

• You have aPhDincomputersciencein the field offormal methods, ideally, with knowledge inRuntime VerificationorModel-Based Testing.
• You also have an interest insoftware engineeringand on applying formal methods on concrete use cases to evaluate theirscaling.
• You enjoydevelopingsoftware tools and haveprogrammingexperience (experience in C++ or Rust would be a plus).

By joining our team, you'll have the opportunity to contribute to the future of real-time verification, making a meaningful difference in the world of distributed systems. If you're passionate about innovation, research, and software development, we encourage you to apply and be part of our exciting journey.

In accordance with the commitments made by the CEA in favor of the integration of people with disabilities, this job is open to everyone.

[1] Mahe, E., Gaston, C., Le Gall, P.: Revisiting semantics of interactions for trace validity analysis. FASE 2020. Springer.

[2] Mahe, E., Bannour, B., Gaston, C., Lapitre, A., Le Gall, P.: A small-step approach to multi-trace checking against interactions. SAC 2021. ACM.