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:

• A cutting-edge research ecosystem, unique in its kind and dedicated to themes of high societal importance, which gives meaning to your mission
• Training to strengthen your skills, acquire new ones and boost your mission
• A work/life balance recognized by our employees
• The possibility of teleworking to balance transport times and contribute to your quality of life
• A works council rich in benefits and social, cultural and sporting activities
• A workplace in the heart of a dynamic plateau, surrounded by schools and tech companies
• A subsidized company restaurant nearby
• A company savings plan with employer contribution
• Public transport costs covered at 75%
• Dedicated shuttles from Paris

REQUIRED SKILLS :

• You have a PhD in computer science in the field of formal methods, ideally, with knowledge in Runtime Verification or Model-Based Testing.
• You also have an interest in software engineering and on applying formal methods on concrete use cases to evaluate their scaling.
• You enjoy developing software tools and have programming experience (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.