Research

Decision process for Logical Time

We are progressing the study of efficient methods for (syntactic) model-based expressiveness and (semantic) analysis/verification of multiform Logical Time (LT) formalisms, centered around our original CCSL constraint language (with possibly relevant extensions/restrictions.

This is a topic of collaboration with Chinese partners, mostly in the context of our associated-team Plot4IoT (see collaboration section). This year we focused on automatic synthesis of safe-timing CCSL constraints 14, as well as the use of reinforcement learning methods for such synthesis 15.

In the continuation of his PhD thesis Pavlo Tokariev studied descriptions of imprecise logical clocks, with notions of logical jitter (accumulative or not), with the impact of such constructs on operational semantics and event-driven simulation sc

Formalizing and extending Smart Contracts languages with temporal and dynamic features

The PhD of Enlin Zhu is funded on the SIM ANR project (see section 9.4), started January 2021. We initially focused mainly on smart contracts and their acceptance by lawyers, but we decided afterwards to consider the distributed application as a whole, since the smart contract itself in isolation is not sufficient to have a global end-to-end control of the services.

The main result is a state-based modeling of the recovery mechanism used in distributed ledger applications. There our formalisms are very relevant to capture both state-dependent properties and (logical) time requirements. This is also a place where the actual implementation and the temporality of the orchestration has a direct impact on the function to be achieved.

It is indeed very good to show the actual benefit in our setting of the model-based approach, allowing to reason and conduct verification at model level, and then hope to synthetize correct-by-construction code. We mainly target the generation of the control part that puts into music the purely functional parts deployed either on smart contracts or on some of the actors of the distributed service (including oracles).

While this result has been submitted twice, it was not yet accepted by a reviewing committee.

CCSL extension to stochastic Logical Time

During this second year of Arseniy Gromovoy PhD thesis, we tried to draw connections between stochastic extensions of our CCSL constraint language and formal models of Functional Safety Analysis. The idea is to combine an abstract modeling of the system predicted nominal behavior, then a superposed stochastic model of rare, faulty behaviors. The purpose of analysis is then to guarantee sufficient dependability probabilities for the compound global system, given hypothesis on the potential local failures (all expressed in logical time terms).

Safety rules for autonomous driving

We had addressed the topic of formal modeling of automotive driving Safety Rules in a previous PhD thesis. In the current PhD of Maksym Labzhaniia we are revisiting this language in the light of logical multi-dimensions, mostly time and space (linked together by speed).

Take-over between automated and human automotive driving

This work was conducted as part of PSPC project ADAVEC, see contracts section 9.5.

The objective of ADAVEC is to study disengagement principles, where driving responsibility may be handed over between either a human driver or an artificial intelligence. This requires the formalization of take-over rules and models, with environmental observations both of the outside road environment, but also the cockpit inside and the human driver state. The postdoctoral period of Ankica Barisic and the temporary research engineer François Revest worked on this project, integrating their results in a general demonstrator developed by the industrial partners 19, 26.

On the generation of compiler friendly C code from CCSL specification

The objective of this work was to produce efficient sequential C codes from a CCSL description. A current prototype tool, named ECOGEN, was completed and intensively tested. ECOGEN can run on four prevalent compilers: GNU gcc, INTEL icc, Clang/LLVM, as well as CompCert by Inria. In addition to the small benchmarks of CCSL at hand, we produce synthetic ones with random generation techniques as well. The next step would be to extend ECOGEN in order to generate tuned parallel C code.

Sadly, the PhD thesis was interrupted in 2023 after Baptiste Allorant resigned for private medical reasons. But his source code and experimental data have been correctly saved on INRIA github.

Behavioral semantics in Model Driven Engineering

In the last years, in collaboration with other academic researchers, we developed the GEMOC studio, a language workbench to develop new modeling or programming languages and their interactions, based on a formal concurrency model. We recently used it for platform based design 21

Two new results emerged this year. First, we figured out that it may be difficult for a user to debug concurrency since depending on the systems, some interleaving are not of interest and make difficult the exploration of significant ones. From these experiments, we decided to built up upon the Debugger Adapter Protocol to allow concurrency debugging. It implies among other a place where exploration strategies can be defined by the user (the user being either the language designer or the system designer). The concurrency strategies hide the irrelevant interleaving to highlight the important ones 17. These strategies are defined independently of the execution engine and implemented into the GEMOC studio. The companion webpage is accessible here.

Second, we investigated further the notion of fidelity of a model with respect to the (knowledge of) reality and its impact in digital twins modeling. It clarifies the notion of model substituability during the development and/or verification process 22. This is specifically addressed in the PhD thesis of Joao Cambeiro, in which we aim to characterize the capacity of distinct models to address a common reality. Defense is expected in the next months.

Efficient parallelism in shared memory

We progressed further the technology underlying the LoPhT tool 6.1.4, partly inside the ANR Caotic project launched this year. We were also granted a bilateral collaborative funding from Airbus for continued evaluation of LoPhT in industrial context.

A language and compiler for embedded and Real-Time Machine Learning programming

This research axis connects three research and engineering fields: Real-Time/Embedded programming, High-Performance Compilation, and Machine Learning. Initiated with the PhD thesis of Hugo Pompougnac (2022), it was extended this year with new exciting ideas allowing to add training features to the previous inference modeling in MLIR internal format representation extended with synchronous notions. This work was conducted with researchers from Google (including Albert Cohen, formerly DR Inria) 31.

The Static Single Assignment (SSA) form has proven an extremely useful tool in the hands of compiler builders. First introduced as an intermediate representation (IR) meant to facilitate optimizations, it became a staple of optimizing compilers. More recently, its semantic properties1 established it as a sound basis for High-Performance Computing (HPC) compilation frameworks such as MLIR, where different abstraction levels of the same application2 share the structural and semantic principles of SSA, allowing them to co-exist while being subject to common analysis and optimization passes (in addition to specialized ones).

But while compilation frameworks such as MLIR concentrate the existing know-how in HPC compilation for virtually every execution platform, they lack a key ingredient needed in the high-performance embedded systems of the future—the ability to represent reactive control and real-time aspects of a system. They do not provide first-class representation and reasoning for systems with a cyclic execution model, synchronization with external time references (logical or physical), synchronization with other systems, tasks and I/O with multiple periods and execution modes.

And yet, while the standard SSA form does not cover these aspects, it shares strong structural and semantic ties with one of the main programming models for reactive real-time systems: dataflow synchrony, and its large and structured corpus of theory and practice of RTE systems design.

Relying on this syntactic and semantic proximity, we have extended the SSA-based MLIR framework to open it to synchronous reactive programming of real-time applications. We illustrated the expressiveness of our extension through the compilation of the pure dataflow core of the Lustre language (see software section for mlirlus 6.1.6). This allowed us to model and compile all data processing, computational and reactive control aspects of a signal processing application3. In the compilation of Lustre (as embedded in MLIR), following an initial normalization phase, all data type verification, buffer synthesis, and causality analysis can be handled using existing MLIR SSA algorithms. Only the initialization analysis specific to the synchronous model (a.k.a. clock calculus or analysis) requires specific handling during analysis and code generation phases, leading to significant code reuse.

The MLIR embedding of Lustre is non-trivial. As modularity based on function calls is no longer natural due to the cyclic execution model, we introduced a node instantiation mechanism. We also generalized the usage of the special undefined/absent value in SSA semantics and in low-level intermediate representations such as LLVM IR. We clarified its semantics and strongly linked it to the notion of absence and the related static analyses (clock calculi) of synchronous languages.

Our extension remains fully compatible with SSA analysis and code transformation algorithms. It allows giving semantics and an implementation to all correct SSA specifications. It also supports static analyses determining correctness from a synchronous semantics point of view.

An ANR project proposal has been submitted, and we participate to the Confiance.AI national initiative (in project EC7 – embedded AI) continues.

Formal verification of Logical Execution Time applications

Fabien Siron defended his PhD on this topic in December 2023 28.

The work, that was started by providing full operational semantics as a synchronous Logical Execution Time formalism (sLET) to the PsyC language 32, was satisfactorily concluded by applying it for model-checking automatic verification, with effective tool support and experimental evaluation on case study 25.

The thesis was funded on a CIFRE contract with the Krono-Safe company, now renamed Asterios Technologies after its acquisition by Safran. The proof-of-concept prototype should be integrated to the PsyC toolsuite.

More checkers targeted were NuXMV, Prover, Uppaaal and Kind2. Translators for interfacing were devised.

Interference analysis in Real-Time task mapping

In this work, funded by the Institut de Recherche Technologique (IRT) Saint-Exupery, and in connection with local R&D labs of Renault Software Factory and Thales Alenia Space, we consider model-based formal engineering of Interface Description Languages (IDL) to support logical time annotations and abstract temporized functional behavior representations. A very pragmatic simulator has been developped. In this simulator, applications are characterized by a temporal profil of their resource usage, the resources are characterized by the number of simultaneous access they support and the result is an evaluation of time spent waiting for a resource for each application.

Trustworthy Fleet deployment and management

This activity is a follow-up of Nicolas Ferry previous activities in ENACT H2020 project, now renewed since his arrival in Kairos in the TrustFleet PHC 9.3.2 and DYNABIC 9.3.1 HEU projects. Continuous and automatic software deployment is still an open question for IoT systems, especially at the Edge and IoT ends. The state-of-the-art Infrastructure as Code (IaC) solutions are established on a clear specification about which part of the software goes to which types of resources. This is based on the assumption that, in the Cloud, one can always obtain the exact computing resources as required. However, this assumption is not valid on the Edge and IoT levels. In production, IoT systems typically contain hundreds or thousands of heterogeneous and distributed devices (also known as a fleet of IoT/Edge devices), each of which has a unique context, and whose connectivity and quality are not always guaranteed. In ENACT, we both investigated the challenge of automating the deployment of software on heterogeneous devices and of managing variants of the software which fit different types or contexts of Edge and IoT devices in the fleet 24. In 2022, GeneSIS (a part of the aforementioned results) was recognized by the EC innovation radar as highly innovant with high maturity level. The natural next step is to investigate how to guarantee the trustworthiness of the deployment when (i) the quality of the devices is not guaranteed, (ii) the context of each device is continuously changing in an unanticipated manner, and (iii) software components are frequently evolving in the whole software stack of each device. In such context, ensuring the proper ordering and synchronization of the deployment actions is critical to improve the quality and trustworthiness and to minimize the downtime.

Model-Based serverless platform for the Cloud-Edge-IoT continuum

One of the most prominent implementation of the serverless programming model is Function-as-a-Service (FaaS). Using FaaS, application developers provide source code of serverless functions, typically describing only parts of a larger application, and define triggers for executing these functions on infrastructure components managed by the FaaS provider. The event-based nature of the FaaS model is a great fit for Internet of Things (IoT) event and data processing. However, there are still challenges that hinder the proper adoption of the FaaS model on the whole IoT-Edge-Cloud continuum. These include (i) vendor lock-in, (ii) the need to deploy and adapt serverless functions as well as their supporting services and software stack to the cyber-physical context in which they will execute, and (iii) the proper orchestration and scheduling of serverless functions deployed on the whole continuum. These observations are being confirmed by our ongoing systematic literature review initiated as part of the TrustFleet PHC aurora project in collaboration with SINTEF (Oslo, Norway), and performed as part of Barbara de Oliveira internship. In parallel, and to address the aforementioned challenges we initiated a first prototyping platform for the design, deployment, as well as maintenance of applications over the IoT-Edge-Cloud continuum. In particular, our platform enables the specification and deployment of serverless functions on Cloud and Edge resources as well as the deployment of their supporting services and software stack over the whole IoT-Edge-Cloud continuum. Next step will be to investigate solutions for the proper and timely orchestration and scheduling of these functions.

Behavioral equivalence of Open Systems

This work is conducted in part jointly with Rabea Ameur-Boulifa, associate professor at Telecom Paris. We consider Open (concurrent) Systems where the environment is represented as a number of processes whose behavior is unspecified. Defining their behavioral semantics and equivalences from a Model-Based Design perspective naturally implies model transformations. To be proven correct, they require equivalence of “Open” terms, in which some individual component models may be omitted. Such models take into account various kind of data parameters, including, but not limited to, time.This year we focused on notions of refinements for Open Terms 29, 18.

A formal framework is developed, as well as related effective tool set 6.1.1, for the compositional analysis of such programs.

After the retirement of Eric Madelaine, activities are still carrying on at Telecom Paris.

Performance evaluation in ETSI oneM2M standard

In the context of the ETSI Testing Task Force (TTF 019) project, we studied performance evaluation of some (but not all) open source implementations of the oneM2M IoT interoperability standard, such as OM2M, OCEAN and ACME.

We first setup few cases studies 33 representating paradigmatic IoT/ CPS systems to be simulated/deployed and finally measured on the basis on a selected choices of KPIs. Then, we contribute with a multi-level model of a oneM2M system including the application behaviour, the oneM2M platform and services, and the oneM2M implementation 34. This model will be injected and measured in the discrete event simulator OMNeT++.

Raising a contact tracing standard to a forecast standard

In the recent past, we standardized  40 a novel contact tracing protocol, called Asynchronous Contact Tracing (ACT). ACT traces the presence of Covid19 virus via the IoT connected sensors and makes those informations available anonymously. This year we extended ACT in order to add a global detection and inter-communication IoT network focused on rapid response to bio-emergencies. This would potentially change the current services already deployed by the National Public Health Institutes to monitor, alert and advise political decision makers, public and military services, environmental institutes and citizens. This extension could promote an ETSI European standard capable of a real-time “forecasting” of any kind of pathogens and pollutions to people in the EU space, in an anonymous, resilient, and secure way; the standard should be sufficiently flexible and customizable nation-by-nation, according to their peculiar laws.

Sources of the web application (front-end and back-end) and the running android app are fully available on gitlab inria, while the web front-end can be runned by now on act.inria.fr. A rich documentation is also available. We are currently in the process of standardizing the extended protocol at the ETSI TC SmartM2M, and we are actively searching for fully fledged realistic big open-data sets in order to stress our proof of concept and our oneM2M architecture on different use cases. We also envisage to scale up the application to a bigger TRL scale by looking for internal (Inria) and external funding.

Strong priority and determinacy in timed CCS

Building on the classical theory of process algebra with priorities, we identify a new scheduling mechanism, called sequentially constructive reduction which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinism-by-construction for multi-cast concurrent communication. In particular, it permits us to model shared memory multi-threading with reaction to absence as it lies at the core of the programming language Esterel.

In the technical setting of CCS extended by clocks and priorities, we prove for a large class of processes, which we call structurally coherent the Church-Rosser confluence property for constructive reductions. We further show that under some syntactic restrictions, called pivotable the operators of prefix, summation, parallel composition, restriction and hiding preserve structural coherence. This covers a strictly larger class of processes compared to those that are confluent in Milner’s classical theory of CCS without priorities 30.

A middleware for the experimentation on IoT mobile networks

In the context of studies on decentralized algorithms from mobile dynamic networks, we investigated the state of the art of the experimentation tools. We discovered that existing solutions, either coming from labs or companies, do not match the requirements of experimentation as it is usually done by Researchers. Indeed commercial products focus on reliability and interoperability at the expense of versatility, while lab tools most often serve as proof of concepts. The experimental study of algorithms requires the availability, in a single solution, of the following features: support for both synchronous and asynchronous communication, simulation/emulation of large systems, fast deployment, Web interoperability, and full decentralization, just to name a few. Idawi was designed and implemented to the very purpose of providing the Research community with a tool tailored to its needs 20. See also the Software section of this report 6.1.7.