Tool supported model completion with support for design pattern application

Generative AI and large language models (LLMs), such Copilot and ChatGPT can complete code based on initial fragments written by a developer. They are integrated in software development environments such as VS code. Many papers analyse the advantages and limitations of these approaches for code generation, see for instance Besides some deficiencies, the produced code is often correct and the results that are getting increasingly better.

However, a surprisingly small amount of work has been done in the context of completion software models (for instance based on UML). The paper concludes that while the performance of the current LLMs for software modeling is still limited (in contrast to code generation), there is a need that (in contrast to code generation) we should adapt our model-based engineering practices to these new assistants and integrate these into MBSE methods and tools.

The integration of design-patterns is a complementary part of this work. Originally coming from building architecture, the term design patterns has been adopted in the software domain to capture a proven solution for a given problem along with its advantages and disadvantages. A bit later, the term anti-pattern has been proposed to identify patterns that are known not to work or having severe disadvantages. Thus, when proposing a completion, then assistant could explicitly reference an existing design pattern with its implications. The completion proposal can be based either on identified model fragments (including modeled requirements) or an explicit pattern selection. This thesis will explore the state-of-the-art of model completion with AI and design patterns and associated tool support. Up to now, little work is available on pattern formalization and the use in model tools. It will propose to identify the modelers intention, based on partial models. The task could be rule-based but should also explore machine-learning approaches. Implement a completion proposal in the context of a design tool, notably Papyrus SW designer. The solution will be evaluated.

Combining over and under-approximations for low-level code analysis

Because program analysis is an undecidable problem, static analyzes fall into 2 categories:
- Sound analyses, which calculate an over-approximation of all the program's behaviors, and make it possible to verify the absence of errors.
- Complete analyses, which calculate an under-approximation of the possible behaviors of the program, and allow errors to be found.

The aim of the thesis is to study this combination of techniques for the verification of low-level programs, in particular binary executables, by targeting in particular the analyzes of memories and control flow, which are the capital information for understanding the possible behaviors of a binary executable.

[POPL'23]: SSA Translation is an Abstract Interpretation, M. Lemerre (Distinguished paper award)
[VMCAI'22]: Lightweight Shape Analysis Based on Physical Types, O. Nicole, M. Lemerre, X. Rival
[RTAS'21]: No Crash, No Exploit: Automated Verification of Embedded Kernels, O. Nicole, M. Lemerre, S. Bardin, X. Rival (best paper award)
[LPAR'18] Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing B. Farinier, S. Bardin, R. David, M. Lemerre

Proof of functional equivalence of binary codes in the context of embedded program hardening

The general context of this thesis is the cyber-security of embedded
systems. The research background of this thesis is tied to the
automatic application of counter-measures against the so-called physical
attacks, which encompass observation attacks (side-channel attacks) and
perturbation attacks (fault-injection attacks).

The CEA List is working on COGITO, a compiler toolchain based on LLVM
for the automatic application of software counter-measures against
physical attacks. Given a source-level implementation of an unprotected
program, our toolchain produces an optimised binary program including
targeted counter-measures, such that the compiled program is hardened
against a specified threat model. Two key points are today crucial to
trust the compiled programs:
1. the proof of robustness of programs produced by our toolchain,
2. the proof that adding counter-measures does not alter the
functionality of the target programs.

This thesis will target the second point: bringing formal guarantees
about the functional correctness of the secured programs. We will use
sound and exhaustive symbolic reasoning, supported by BINSEC
(). BINSEC is an open-source toolset
developed at CEA List to help improve software security at the binary
level. It relies on cutting-edge research in binary code analysis, at
the intersection of formal methods, program analysis, security and
software engineering.

The PhD thesis will be hosted at the CEA in Saclay, within the BINSEC team.
Short-term stays
at CEA Grenoble will be planned throughout the three
years of the thesis to collaborate with experts and developers of

Artful guidance of test generation tools

Fuzzing is an automatic test generation technique. It consists in repeatedly executing a program with automatically generated inputs, in order to trigger crashes, symptoms of underlying bugs in the code, which can then be fixed. A major challenge in this area is moving from indiscriminate exploration of how programs work to artful guidance towards the discovery of important bugs. Taking advantage of the expertise of our team and our previous work, the objective of the thesis is to propose, implement and evaluate means to meet this challenge, taking advantage of finer-grained guidance mechanisms.

Deep Neural Network Uncertainty Estimation on Embedded Targets

Over the last decade, Deep NeuralNetworks (DNNs) have become a popular choice to implement Learning-Enabled Components LECs in automated systems thanks to their effectiveness in processing complex sensory inputs, and their powerful representation learning that surpasses the performance of traditional methods. Despite the remarkable progress in representation learning, DNNs should also represent the confidence in their predictions to deploy them in safety-critical systems. Bayesian Neural Networks (BNNs) offer a principled framework to model and capture uncertainty in LECs. However, exact inference in BNNs is difficult to compute. Thus, we rely on sampling techniques to approximate the true posterior of the weights for computing the posterior predictive distribution (inference). In this regard, relatively simple though computationally and memory expensive sample-based methods have been pro posed for approximate Bayesian inference to quantify uncertainty in DNNs, e.g., Monte-Carlo dropout or Deep Ensembles. Efficient DNN uncertainty estimation in resource-constrained hardware platforms remains an open problem, limiting the adoption within applications from highly automated systems that possess strict computation and memory budgets, tight time constraints, and safety requirements. This thesis aims to develop novel methods and hardware optimizations for efficient and reliable uncertainty estimation in modern DNN architectures deployed in hardware platforms with limited computation resources.

Scenario-Based Testing for Automated Systems: Enhancing Safety and Reliability in Compliance with Regulations and Standards

This research aims to investigate the effectiveness of scenario-based testing as a comprehensive and robust approach for evaluating ASs' performance while enhancing their safety and reliability with respect to regulations and standards.
The primary objective of this thesis will be to investigate the benefits of scenario-based testing for automated systems and its compliance with regulations and standards. The following sub-objectives will be pursued:
- Conduct an in-depth review of relevant literature and industry practices on ASs testing methodologies, with a focus on the unique challenges posed by ASs' complex decision-making algorithms and interaction with the dynamic environment.
- Develop a scenario-based testing framework for systematic identification, generation, selection, and execution of realistic and diverse scenarios, for automated systems
- Analyze gaps or areas of non-compliance about the key concepts and requirements outlined in regulations and standards and examine their applicability, implications and improvments for scenario-based testing.
- Conduct extensive validation of the proposed scenario-based testing framework through different real-world and near-realistic transportation applications (various types, varying levels of automation, and diverse real-world scenarios) to evaluate the practical applicability and benefits of the methodology.
The findings and recommendations from this research will ultimately guide AV manufacturers, regulators, and stakeholders in developing and validating ASs that comply with the regulatory framework, fostering the safe and responsible deployment of automated systems in the future.