2023Activity reportProject-TeamKAIROS

3.1 Cyber-Physical co-modeling

In Real-Time embedded systems, timing criticality imposes to take time predictivity as much into account as functional determinism, and this from the very beginning design phases onward. In addition, cyber-Physical System modeling requires joint representation of digital/cyber controllers and natural physics environments. Heterogeneous modeling must then be articulated to support accurate (co-)simulation, (co-)analysis, and (co-)verification, with multiple logical time sources and scales.

Figure 1 sketches the overall design framework. It comprises functional requirements, to be met provided surrounding platform guarantees, in a contract approach. All relevant aspects are modeled with proper Domain Specific Languages (DSL), so that constraints can be gathered globally, then analyzed to build a mapping proposal with both a structural aspect (functions allocated to platform resources), but also behavioral ones, scheduling activities. Mapping may be computed automatically or not, provably correct or not, obtained by static analytic methods or abstract execution.

Physical phenomena (in a very broad acceptance of the term) are usually modeled using continuous-time models and differential equations. Then the “proper” discretization opportunities for numerical simulation form a large spectrum of mathematical engineering practices. Note that is not at all the domain of expertise of Kairos members, but it should not be a limitation as long as one can assume a number of properties from the discretized version. On the other hand, we do have a strong expertise on modeling of both embedded processing architectures and embedded software (i.e., the kind of usually concurrent, sometimes distributed software that reacts to and control the physical environment). This is important as, unlike in the “physical” areas where modeling is common-place, modeling of software and programs is far from mainstream in the Software Engineering community. These domains are also an area of computer science where modeling, and even formal modeling, of the real objects that are originally of discrete/cyber nature, takes some importance with formal Models of Computation and Communications. It seems therefore quite natural to combine physical and cyber modeling in a more global design approach (even multi-physic domains and systems of systems possibly, but always with software-intensive aspects involved).

Our objective is certainly not to become experts in physical modeling and/or simulation process, but to retain from it only the essential and important aspects to include them into System-Level Engineering design, based on Model-Driven approaches allowing formal analysis.

This sets an original research agenda: Model-Based System Engineering environments exist, at various stages of maturity and specificity, in the academic and industrial worlds. Formal Methods and Verification/Certification techniques also exist, but generally in a point-wise fashion. Our approach aims at raising the level of formality describing relevant features of existing individual models, so that formal methods can have a greater general impact on usual, “industrial-level”, modeling practices. Meanwhile, the relevance of formal methods is enhanced as it now covers various aspects in a uniform setting (timeliness, energy budget, dependability, safety/security...).

Directions on formalizing CPS should focus on the introduction of uncertainty (stochastic models) in our particular framework, on relations between (logical) real-time and security, and on accounting for resource discovery also in presence of mobility inherent to connected objects and Internet of Things 2.

3.2 Cyber-Physical co-simulation

The FMI standard (Functional Mock-Up Interface) has been proposed for “purely physical” (i.e., based on persistent signals) co-simulation, and then adopted in over 100 industrial tools including frameworks such as Matlab/Simulink and Ansys, to mention two famous model editors. With the recent use of co-simulation to cyber-physical systems, dealing with the discrete and transient nature of cyber systems became mandatory.

Together with other people from our community, we showed that FMI and other frameworks for co-simulation badly support co-simulation of cyber-physical systems; leading to bad accuracy and performances. More precisely, the way to interact with the different parts of the co-simulation require a specific knowledge about its internal semantics and the kind of data exposed (e.g., continuous, piecewise-constant). Towards a better co-simulation of cyber-physical systems, we are looking for conservative abstractions of the parts and formalisms that aim to describe the functional and temporal constraints that are required to bind several simulation models together.

3.3 Formal analysis and verification

Because the nature of our constraints is specific, we want to adjust verification methods to the goals and expressiveness of our modeling approach 13. Quantitative (interval) timing conditions on physical models combined with (discrete) cyber modes suggest the use of SMT (Satisfiability Modulo Theories) automatic solvers, but the natural expressiveness requested (as for instance in our CCSL constructs) shows this is not always feasible. Either interactive proofs, or suboptimal solutions (essentially resulting of abstract run-time simulations) should be considered.

Complementarily to these approaches, we are experimenting with new variants of symbolic behavioural semantics, allowing to construct finite representations of the behaviour of CPS systems with explicit handling of data, time, or other non-functional aspects 4.

3.4 Relation between model and code

While models considered in Kairos can also be considered as executable specifications (through abstract simulation schemes), they can also lead to code synthesis and deployment. Conversely, code execution of smaller, elementary software components can lead to performance estimation enriching the models before global mapping optimization 3.

CPS introduce new challenging problems for code performance stability. Indeed, two additional factors for performance variability appear, which were not present in classical embedded systems: 1) variable and continuous data input from the physical world and 2) variable underlying hardware platform. For the first factor, CPS software must be analyzed in conjunction with its data input coming from the physics, so the variability of the performance may come from the various data. For the second factor, the underlying hardware of the CPS may change during the time (new computing actors appear or disappear, some actors can be reconfigured during execution). The new challenge is to understand how these factors influence performance variability exactly, and how to provide solutions to reduce it or to model it. The modeling of performance variability becomes a new input.

3.5 Code generation and optimization

A significant part of CPS design happens at model level, through activities such as model construction, analysis, or verification. However, in most cases the objective of the design process is implementation. We mostly consider the implementation problem in the context of embedded, real-time, or edge computing applications, which are subject to stringent performance, embedding, and safety non-functional requirements.

The implementation of such systems usually involves a mix of synthesis—(real-time) scheduling, code generation, compilation—and performance (e.g. timing) analysis, as introduced in 7. One key difficulty here is that synthesis and performance analysis depend on each other. As enumerating the various solutions is not possible for complexity reasons, heuristic implementation methods are needed in all cases. One popular solution here is to build the system first using unsafe performance estimations for its components, and then check system schedulability through a global analysis. Another solution is to use safe, over-approximated performance estimations and perform their mapping in a way that ensures by construction the schedulability of the system.

In both cases, the level of specification for the compound design space -including functional application, execution platform, extra-functional requirements, implementation representation is a key problem. Another problem is the definition of scalable and efficient mapping methods based on both "exact" approaches (ILP/SMT/CP solving) and compilation-like heuristics.

3.6 Extensions for spatio-temporal modeling and mobile systems

While Time is clearly a primary ingredient in the proper design of CPS systems, in some cases Space, and related notions of local proximity or conversely long distance, play also a key role for correct modeling, often in part because of the constraints this puts on interactions and time for communications. Once space is taken into account, one has to recognize also that many systems will request to consider mobility, originated as change of location through time. Mobile CPSs (or mCPS) occur casually in real-life, e.g., in the case of Intelligent Transportation Systems, or roaming connected objects of the IoT.

Spatio-temporal and mobility modeling may each lead to dynamicity in the representation of constraints, with the creation-deletion-discovering of new components in the system. This opportunity for new expressiveness will certainly cause new needs in handling constraint systems and topological graph locations. The new challenge is to provide an algebraic support with a constraint description language that could be as simple and expressive as possible, and of use in the semantic annotations for mobile CPS design. We also aim to provide fully distributed routing protocols to manage Semantic Resource Discovery in IoT and to standardize it.

3.7 Towards foundations for synchronous algorithmic & proof languages

The challenge is to find new process algebras with related type systems able to specify dynamic (operational semantics) and static (type systems) semantics of synchronous languages and algorithms. Adding types to such algebra would allow to certify them through Interactive Theorem Provers (ITP).

Luigi Liquori holds expertise in working in and extending the Edinburgh Logical Framework (LF), itself the basis of almost all ITPs 5. New notions of synchronizing proofs could be introduced in LF to cope with these timed process algebras, and so help reasoning on (future evolutions of?) synchronous programming languages.

3.8 IoT and CPS standardization

Under the shield of the ETSI standardization consortium, we study protocols, models and performances of widely used CPS, mCPS and IoT frameworks and protocols: we focus on oneM2M ETSI interoperability standards in many aspects, see relevant sections on application domains 4.4, new results 7.15 7.16, and contracts 9.3.2 9.3.2.

4.1 Cyber-Physical and embedded system design

System Engineering for CPS systems requires combinations of models, methods, and tools owing to multiple fields, software and system engineering methodologies as well as various digitalization of physical models (such as "Things", in Internet of Things (IoT)). Such methods and tools can be academic prototypes or industry-strength offers from tool vendors, and prominent companies are defining design flow usages around them.

We have historical contacts with industrial and academic partners in the domains of avionics and embedded electronics (Airbus, Thales, Safran). We also have new collaborations in the fields of satellites (Thales_Alenia_Space) and connected cars driving autonomously (Renault Software Factory). These provide us with current use cases and new issues in CPS co-modeling and co-design (Digital Twins) further described in New Results section. The purpose here is to insert our formal methods into existing design flows, to augment their analysis power where and when possible.

4.2 Safe driving rules for automated driving

Self-driving cars will have to respect roughly the same safety-driving rules as currently observed by human drivers (and more). These rules may be expressed syntactically by temporal constraints (requirements and provisions) applied to the various meaningful events generated as vehicles interact with traffic signs, obstacles and other vehicles, distracted drivers and so on. We feel our formalisms based on Multiform Logical Time to be well suited to this aim, and follow this track in several collaborative projects with automotive industrial partners. This domain is an incentive to increase the expressiveness of our language and test the scalability of our analysis tools on real size data and scenari.

4.3 Smart contracts for IoT objects

In collaboration with local industrial and standardisation partners, we have considered Smart Contracts (SC), as a way to formally establish specification of behavioral system traces, applied to connected objects in an IoT environment.

The ANR project SIM (see contract section) is based on the definition of formal language to describe services for autonomous vehicles that would execute automatically based on the observation of what is happening on the vehicle or the driver. The key focus is on the design of a virtual passport for autonomous cars that would register the main events occurring on the car and would use them to operate automatic but trustworthy and reliable services.

In a distinct effort, we investigate ways to "cleanly" extend smart contract languages with the capacity of modification/update at run-time, for the dynamic correction of errors or vulnerabilities (see next subsection on standardization). This direction is based on former work by L. Liquori and coauthors  41, 36.

4.4 oneM2M and ETSI standards

We participate to several ETSI Standardisation Committees:

• Based on our skills in IoT Semantic Discovery Protocols  39, 38 and content-based network protocols  35, 37 we contribute to the SmartM2M standard enhancement.
• In the new TTF (Testing Task Force) 019 project we consider as performance evaluation, analysis, planning and deployment for some (but not all) oneM2M open source implementations.
• A new STF (Specialist Task Force) ETSI project will explore the requirements of Smart Contrats from the UE Data Act and the UE EIDAS2 proposal. We contribute in definition of Smart Contracts that support exchange of data and their remuneration, with compliance versus new European Digital Identity and Electronic Ledger frameworks as target.
• Following our previous standardization effort of Asynchronous Contact Tracing (ACT) 40 in the Covid19 virus context, we now extend to the standardization of a new Asynchronous Forecast Standard, still at ETSI. The ambitious goal of designing an IoT eHealth standard, that can enable multiple detection and surveillance platforms to communicate and cooperate together, requires the multidisciplinary interaction between public agencies and biotech companies.

5.1 Footprint of research activities

• Julien DeAntoni and Frédéric Mallet are members of the I3S Working Group on new practical ways to measure and reduce the impact of our research activity on the environment.

6.1 New software

7.1 Decision process for Logical Time

Participants: Frédéric Mallet, Pavlo Tokariev, Robert de Simone.

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

7.2 Formalizing and extending Smart Contracts languages with temporal and dynamic features

Participants: Frédéric Mallet, Enlin Zhu.

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.

7.3 CCSL extension to stochastic Logical Time

Participants: Robert de Simone, Arseniy Gromovoy.

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

7.4 Safety rules for autonomous driving

Participants: Frédéric Mallet, Maksym Labzhaniia, Marie-Agnès Peraldi-Frati, Julien Deantoni, Robert De Simone.

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

7.5 Take-over between automated and human automotive driving

Participants: Robert de Simone, François Revest, Ankica Barisic, Julien Deantoni.

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.

7.6 On the generation of compiler friendly C code from CCSL specification

Participant: Baptiste Allorant, Sid Touati, Frédéric Mallet.

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.

7.7 Behavioral semantics in Model Driven Engineering

Participants: Julien Deantoni, Joao Cambeiro.

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.

7.8 Efficient parallelism in shared memory

Participant: Dumitru Potop Butucaru.

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.

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

Participants: Dumitru Potop Butucaru.

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.

7.10 Formal verification of Logical Execution Time applications

Participants: Robert de Simone, Dumitru Potop Butucaru, Fabien Siron.

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.

7.11 Interference analysis in Real-Time task mapping

Participants: Julien Deantoni, Robert de Simone.

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.

7.12 Trustworthy Fleet deployment and management

Participants: Nicolas Ferry, Marie-Agnès Peraldi Frati, Julien Deantoni.

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.

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

Participants: Nicolas Ferry, Barbara de Oliveira.

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.

7.14 Behavioral equivalence of Open Systems

Participant: Eric Madelaine.

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.

7.15 Performance evaluation in ETSI oneM2M standard

Participants: Luigi Liquori, Marie-Agnès Peraldi Frati.

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

7.16 Raising a contact tracing standard to a forecast standard

Participants: Luigi Liquori, Antoine Fadda Rodriguez, Antoine Maistre, Alessio Di Dio, Pascal Tempier, Enrico Scarrone.

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.

7.17 Strong priority and determinacy in timed CCS

Participants: Luigi Liquori, Michael Mendler, Robert De Simone.

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.

7.18 A middleware for the experimentation on IoT mobile networks

Participant: Luc Hogie.

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.

9.1 International initiatives

9.2 International research visitors

9.3 European initiatives

9.4 National initiatives

9.5 Regional initiatives

10.1 Promoting scientific activities

10.2 Teaching - Supervision - Juries

10.3 Popularization

11.1 Major publications

• 1 incollectionC.Charles André, J.Julien Deantoni, F.Frédéric Mallet and R.Robert De Simone. The Time Model of Logical Clocks available in the OMG MARTE profile.Synthesis of Embedded Software: Frameworks and Methodologies for Correctness by ConstructionChapter 7Springer Science+Business Media, LLC 2010July 2010, 28HALback to text
• 2 articleY.Y. Bao, M.Mingsong Chen, Q.Q. Zhu, T.T. Wei, F.Frédéric Mallet and T.T. Zhou. Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems3612December 2017, 1989--2002URL: https://hal.inria.fr/hal-01644285DOIback to text
• 3 articleT.Thomas Carle, D.Dumitru Potop-Butucaru, Y.Yves Sorel and D.David Lesens. From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation *.Leibniz Transactions on Embedded SystemsNovember 2015HALDOIback to text
• 4 inproceedingsL.Ludovic Henrio, E.Eric Madelaine and M.Min Zhang. A Theory for the Composition of Concurrent Processes.36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)LNCS-9688Formal Techniques for Distributed Objects, Components, and SystemsHeraklion, Greece2016, 175-194HALDOIback to text
• 5 articleF.Furio Honsell, L.Luigi Liquori, P.Petar Maksimovic and I.Ivan Scagnetto. LLFP : A Logical Framework for modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads.Logical Methods in Computer ScienceFebruary 2017HALback to text
• 6 inproceedingsF.Furio Honsell, L.Luigi Liquori, C.Claude Stolze and I.Ivan Scagnetto. The Delta-framework.38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS) 201812238th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCSAhmedabad, India2018, 37:1--37:21HALDOI
• 7 inproceedingsF.Fatma Jebali and D. P.Dumitru Potop Butucaru. Ensuring Consistency between Cycle-Accurate and Instruction Set Simulators.18th International Conference on Application of Concurrency to System Design, ACSD 2018, Bratislava, Slovakia, June 25-29, 20182018, 105--114URL: https://doi.ieeecomputersociety.org/10.1109/ACSD.2018.00019DOIback to text
• 8 inproceedingsL.Luigi Liquori and C.Claude Stolze. The Delta-calculus: syntax and types.FSCD 2019 - 4th International Conference on Formal Structures for Computation and DeductionDortmund, Germany2019HALDOI
• 9 articleF.Frédéric Mallet and R.Robert De Simone. Correctness issues on MARTE/CCSL constraints.Science of Computer Programming106August 2015, 78--92URL: https://hal.inria.fr/hal-01257978DOIback to text
• 10 articleJ.-V.Jean-Vivien Millo and R.Robert De Simone. Periodic scheduling of marked graphs using balanced binary words.Theoretical Computer Science4582November 2012, 113-130HALDOIback to text
• 11 incollectionD.Dumitru Potop-Butucaru, R.Robert De Simone and J.-P.Jean-Pierre Talpin. Synchronous hypothesis and polychronous languages.Embedded Systems Design and VerificationCRC Press2009, 6-1-6-27HALDOIback to text
• 12 inproceedingsC.Claude Stolze and L.Luigi Liquori. A Type Checker for a Logical Framework with Union and Intersection Types.FSCD 2020 - 5th International Conference on Formal Structures for Computation and DeductionParis, France2020HALDOI
• 13 articleM.Min Zhang, F.Feng Dai and F.Frédéric Mallet. Periodic scheduling for MARTE/CCSL: Theory and practice.Science of Computer Programming154March 2018, 42--60HALDOIback to text

11.2 Publications of the year

11.3 Cited publications

• 35 articleR.Raphael Chand, M.Michel Cosnard and L.Luigi Liquori. Powerful Resource Discovery for Arigatoni Overlay Network.Future Generation Computer Systems241January 2008, 31-48HALDOIback to text
• 36 articleA.Alberto Ciaffaglione, P.Pietro Di Gianantonio, F.Furio Honsell and L.Luigi Liquori. A prototype-based approach to object evolution.The Journal of Object Technology204December 2020, 1--24HALback to text
• 37 inproceedingsL.Luigi Liquori, D.Diego Borsetti, C.Claudio Casetti and C.-F.Carla-Fabiana Chiasserini. An Overlay Architecture for Vehicular Networks.NETWORKING 2008. Ad Hoc and Sensor Networks, Wireless Networks, Next Generation Internet 7th International IFIP-TC6 Networking Conference Singapore, May 5-9, 2008 Proceedings4982Lecture Notes in Computer ScienceSingapore, SingaporeSpringer VerlagMay 2008, 60-71HALDOIback to text
• 38 miscL.Luigi Liquori, M.-A.Marie-Agnès Peraldi-Frati, A.Andrea Cimmino, R.Raúl Garc\'ia Castro, A. Q.Abdul Qadir Khan, S.Sara El Khatab, O.Oleksii Khramov, E.Enrico Scarrone and J.Joachim Koss. ETSI SmartM2M Technical Report 103716; oneM2M Discovery and Query solution(s) simulation and performance evaluation.oneM2M has currently native discovery capabilities that work properly only if the search is related to specific known sources of information (e.g. searching for the values of a known set of containers) or if the discovery is well scoped and designed (e.g. the lights in a house). When oneM2M is used to discover wide sets of data or unknown sets of data, the functionality is typically integrated by ad hoc applications that are expanding the oneM2M functionality. This means that this core function may be implemented with different flavours and this is not optimal for interworking and interoperability.The objective of the present document [i.3] in conjunction with three other ones ETSI TR 103 714 [i.1], ETSITR 103 715 [i.2] and ETSI TR 103 717 [i.4] is the study and development of semantic Discovery and Query capabilities for oneM2M and its contribution to the oneM2M standard.The goal is to enable an easy and efficient discovery of information and a proper interworking with external source/consumers of information (e.g. a distributed data base in a smart city or in a firm), or to directly search information in the oneM2M system for big data purposes.A simulation phase is conducted in parallel and ''circular'' feedback with respect to the study phase, with the goal to provide a proof of concept, run suitable scenarios provided by previous phases and a performance evaluation to support the selection/development of the Discovery and Query solution. The simulator and the simulation results are documented in ETSI TR 103 716 [i.3] (the present document). An extract of the simulation results is included ETSI TR 103 715 [i.2] and ETSI TR 103 717 [i.4]. A selection of the use cases includes a set of oneM2M relevant configurations scenarios to be considered for the simulation activity described below.June 2021HALback to text
• 39 miscL.Luigi Liquori, E.Enrico Scarrone, M.-A.Marie-Agnès Peraldi-Frati, S. M.Seung Myeong Jeong, A.Andrea Cimmino, R.Raúl Garc\'ia Castro, J.Joachim Koss, A. Q.Abdul Qadir Khan, S.Sunil Kumar and S.Sara El Khatab. ETSIETSI SmartM2M Technical Report 103715; Study for oneM2M; Discovery and Query solutions analysis & selection.The oneM2M system has implemented basic native discovery capabilities. In order to enhance the semantic capabilities of the oneM2M architecture by providing solid contributions to the oneM2M standards, four Technical Reports have been developed. Each of them is the outcome of a special study phase: requirements, study, simulation and standardization phase. The present document covers the second phase and provides the basis for the other documents. It identifies, defines and analyses relevant approaches with respect to the use cases and requirements developed in ETSI TR 103 714 The most appropriate one will be selected.January 2021HALback to text
• 40 miscL.Luigi Liquori, E.Enrico Scarrone, S.Suno Wood, L.Lanting Cees, F.Francisco Dasilva, M.Markus Maass, F.Flynn Bob, T.Thomas Kessler, H.Holoyad Taras and M.Massimo Vanetti. ETSIETSI Technical Specification TS 103757. SmartM2M; Asynchronous Contact Tracing System.December 2021HALback to textback to text
• 41 articleL.Luigi Liquori and A.Arnaud Spiwack. FeatherTrait: A Modest Extension of Featherweight Java.ACM Transactions on Programming Languages and Systems (TOPLAS)302March 2008, 11:1--11:32HALDOIback to text