2.1 Introduction

An embedded architecture is an artifact of heterogeneous constituents and at the crossing of several design viewpoints: software, embedded in hardware, interfaced with the physical world. Time takes different forms when observed from each of these viewpoints: continuous or discrete, event-based or time-triggered: modeling and programming formalisms that represent software, hardware and physics significantly alter this perception of time. Therefore, time reasoning in system design is usually isolated to a specific design problem: simulation, profiling, performance, scheduling, parallelization, simulation. The aim of project-team TEA is to define conceptually unified frameworks for reasoning on composition and integration in cyber-physical system design, and to put this reasoning to practice by revisiting analysis and synthesis issues in real-time system design with soundness and compositionality gained from formalization.

2.2 Context

In the construction of complex systems, information technology (IT) has become a central force of revolutionary changes, driven by the exponential increase of computational power. In the field of telecommunication, IT provides the necessary basis for systems of networked distributed applications. In the field of control engineering, IT provides the necessary basis for embedded control applications. The combination of telecommunication and embedded systems into networked embedded systems opens up a new range of systems, capable of providing more intelligent functionalities, thanks to information and communication (ICT). Networked embedded systems have revolutionized several application domains: energy networks, industrial automation and transport systems.

20th-century science and technology brought us effective methods and tools for designing both computational and physical systems, such as for instance Simulink and Matlab. But the design of cyber-physical systems (CPS) is much more than the union of those two fields. Traditionally, information scientists only have a hazy notion of requirements imposed by the physical environment of computers. Similarly, mechanical, civil, and chemical engineers view computers strictly as devices executing algorithms. CPS design is, to date, mostly executed in this ad-hoc manner, without sound, mathematically grounded, integrative methodology. A new science of CPS design will allow to create machines with complex dynamics and high control reliability, and apply to new industries and applications, such as IoT or edge devices, in a reliable and economically efficient way. Progress requires nothing less than the construction of a new science and technology foundation for CPS that is simultaneously physical and computational.

2.3 Motivations

Beyond the buzzword, a CPS is an ubiquitous object of our everyday life. CPSs have evolved from individual independent units (e.g an ABS brake) to more and more integrated networks of units, which may be aggregated into larger components or sub-systems. For example, a transportation monitoring network aggregates monitored stations and trains through a large scale distributed system with relatively high latency. Each individual train is being controlled by a train control network, each car in the train has its own real-time bus to control embedded devices. More and more, CPSs are mixing real-time low latency technology with higher latency distributed computing technology.

In the past 15 years, CPS development has moved towards Model Driven Engineering (MDE). With MDE methodology, first all requirements are gathered together with use cases, then a model of the system is built (sometimes several models) that satisfy the requirements. There are several modeling formalisms that have appeared in the past ten years with more or less success. The most successful are the executable models 123, i.e., models that can be simulated, exercised, tested and validated. This approach can be used for both software and hardware.

A common feature found in CPSs is the ever presence of concurrency and parallelism in models. Large systems are increasingly mixing both types of concurrency. They are structured hierarchically and comprise multiple synchronous devices connected by buses or networks that communicate asynchronously. This led to the advent of so-called GALS (Globally Asynchronous, Locally Synchronous) models, or PALS (Physically Asynchronous, Logically Synchronous) systems, where reactive synchronous objects are communicating asynchronously. Still, these infrastructures, together with their programming models, share some fundamental concerns: parallelism and concurrency synchronization, determinism and functional correctness, scheduling optimality and calculation time predictability.

Additionally, CPSs monitor and control real-world processes, the dynamics of which are usually governed by physical laws. These laws are expressed by physicists as mathematical equations and formulas. Discrete CPS models cannot ignore these dynamics, but whereas the equations express the continuous behavior usually using real numbers (irrational) variables, the models usually have to work with discrete time and approximate floating point variables.

2.4 Challenges

A cyber-physical, or reactive, or embedded system is the integration of heterogeneous components originating from several design viewpoints: reactive software, some of which is embedded in hardware, interfaced with the physical environment through mechanical parts. Time takes different forms when observed from each of these viewpoints: it is discrete and event-based in software, discrete and time-triggered in hardware, continuous in mechanics or physics. Design of CPS often benefits from concepts of multiform and logical time(s) for their natural description. High-level formalisms used to model software, hardware and physics additionally alter this perception of time quite significantly.

In model-based system design, time is usually abstracted to serve the purpose of one of many design tasks: verification, simulation, profiling, performance analysis, scheduling analysis, parallelization, distribution, or virtual prototyping. For example in non-real-time commodity software, timing abstraction such as number of instructions and algorithmic complexity is sufficient: software will run the same on different machines, except slower or faster. Alternatively, in cyber-physical systems, multiple recurring instances of meaningful events may create as many dedicated logical clocks, on which to ground modeling and design practices.

Time abstraction increases efficiency in event-driven simulation or execution (i.e SystemC simulation models try to abstract time, from cycle-accurate to approximate-time, and to loosely-time), while attempting to retain functionality, but without any actual guarantee of valid accuracy (responsibility is left to the model designer). Functional determinism (a.k.a. conflict-freeness in Petri Nets, monotonicity in Kahn PNs, confluence in Milner's CCS, latency-insensitivity and elasticity in circuit design) allows for reducing to some amount the problem to that of many schedules of a single self-timed behavior, and time in many systems studies is partitioned into models of computation and communication (MoCCs). Multiple, multiform time(s) raises the question of combination, abstraction or refinement between distinct time bases. The question of combining continuous time with discrete logical time calls for proper discretization in simulation and implementation. While timed reasoning takes multiple forms, there is no unified foundation to reasoning about multi-form time in system design.

The objective of project-team TEA is henceforth to define formal models for timed quantitative reasoning, composition, and integration in embedded system design. Formal time models and calculi should allow us to revisit common domain problems in real-time system design, such as time predictability and determinism, memory resources predictability, real-time scheduling, mixed-criticality and power management; yet from the perspective gained from inter-domain timed and quantitative abstraction or refinement relations. A regained focus on fundamentals will allow to deliver better tooled methodologies for virtual prototyping and integration of embedded architectures.

3.1 Previous Works

The challenges of team TEA support the claim that sound Cyber-Physical System design (including embedded, reactive, and concurrent systems altogether) should consider multi-form time models as a central aspect. In this aim, architectural specifications found in software engineering are a natural focal point to start from. Architecture descriptions organize a system model into manageable components, establish clear interfaces between them, collect domain-specific constraints and properties to help correct integration of components during system design. The definition of a formal design methodology to support heterogeneous or multi-form models of time in architecture descriptions demands the elaboration of sound mathematical foundations and the development of formal calculi and methods to instrument them.

System design based on the “synchronous paradigm” has focused the attention of many academic and industrial actors on abstracting non-functional implementation details from system design. This elegant design abstraction focuses on the logic of interaction in reactive programs rather than their timed behavior, allowing to secure functional correctness while remaining an intuitive programming model for embedded systems. Yet, it corresponds to embedded technologies of single cores and synchronous buses from the 90s, and may hardly cover the semantic diversity of distribution, parallelism, heterogeneity, of cyber-physical systems found in 21st century Internet-connected, true-time${}^{TM}$-synchronized clouds, of tomorrow's grids.

By contrast with a synchronous hypothesis, yet from the same era, the polychronous MoCC is inherently capable of describing multi-clock abstractions of GALS systems. Polychrony is implemented in the data-flow specification language Signal, available in the Eclipse project POP 4 and in the CCSL standard 5 available from the TimeSquare project. Both provide tooled infrastructures to refine high-level specifications into real-time streaming applications or locally synchronous and globally asynchronous systems, through a series of model analysis, verification, and synthesis services. These tool-supported refinement and transformation techniques can assist the system engineer from the earliest design stages of requirement specification to the latest stages of synthesis, scheduling and deployment. These characteristics make polychrony much closer to the required semantic for compositional, refinement-based, architecture-driven, system design.

While polychrony was a step ahead of the traditional synchronous hypothesis, CCSL is a leap forward from synchrony and polychrony. The essence of CCSL is “multi-form time” toward addressing all of the domain-specific physical, electronic and logical aspects of cyber-physical system design.

3.2 Timed Modeling

To formalize timed semantics for system design, we shall rely on algebraic representations of time as clocks found in previous works and introduce a paradigm of "time system": refinement types that represent timed behaviors. Just as a type system abstracts data carried along operations in a program, a “time system” abstracts the causal interaction of that program module or hardware element with its environment, its pre- and post-conditions, its assumptions and guarantees, either logical or numerical, discrete or continuous. Some fundamental concepts of thelogics we envision are present in the clock calculi found in data-flow synchronous languages like Signal or Lustre, yet bound to a particular model of timed concurrency.

In particular, the principle of refinement type systems 6, is to associate information (data-types) inferred from programs and models with properties pertaining, for instance, to the algebraic domain on their value, or any algebraic property related to its computation: effect, memory usage, pre-post condition, value-range, cost, speed, time, temporal logic 7. Being grounded on type and domain theories, such type systems system should naturally be equipped with program analysis techniques based on type inference (for data-type inference) or abstract interpretation (for program properties inference) to help establish formal relations between heterogeneous component “types”.

Gaining scalability requires the capacities to modularly decompose systems which can be obtained using Abadi and Lamport's concepts of “Composing Specifications” and implemented by the notion of assume-guarantee contracts or Dijkstra monads. Verification problems encompassing heterogeneously timed specifications are common and of great variety: checking correctness between abstract (e.g. the synchronous hypothesis) and concrete time models (e.g. real-time architectures) relates to desynchronisation (from synchrony to asynchrony) and scheduling analysis (from synchronous data-flow to hardware). More generally, they can be perceived from heterogeneous timing viewpoints (e.g. mapping a synchronous-time software on a real-time middle-ware or hardware).

This perspective demands capabilities to use abstraction and refinement mechanisms for time models (using simulation, refinement, bi-simulation, equivalence relations) but also to prove more specific properties (synchronization, determinism, endochrony). All this formalization effort will allow to effectively perform the tooled validation of common cross-domain properties (e.g. cost v.s. power v.s. performance v.s. software mapping) and tackle problems such as these integrating constraints of battery capacity, on-board CPU performance, available memory resources, software schedulability, to logical software correctness and plant controllability.

3.3 Modeling Architectures

To address the formalization of such cross-domain case studies, modeling the architecture formally plays an essential role. An architectural model represents components in a distributed system as boxes with well-defined interfaces, connections between ports on component interfaces, and specifies component properties that can be used in analytical reasoning about the model. Several architectural modeling languages for embedded systems have emerged in recent years, including the SAE AADL 8, SysML 9, UML MARTE 10.

In system design, an architectural specification serves several important purposes. First, it breaks down a system model into components of manageable size and complexity, to establish clear interfaces between components. In this way, complexity becomes manageable by hiding details that are not relevant at a given level of abstraction. Clear, formally defined, and semantically rich component interfaces facilitate integration by allowing most validation efforts to be conducted modularly. Connections between components, which specify how components interact with each other, help propagate the guaranteed effects of a component to the assumptions of linked components.

Most importantly, an architectural model is a repository to share knowledge about the system being designed. This knowledge can be represented as requirements, design artifacts, component implementations, held together by a structural backbone. Such a repository enables automatic generation of analytical models for different aspects of the system, such as timing, reliability, security, performance, energy, etc. Since all the models are generated from the same source, the consistency of assumptions w.r.t. guarantees, of abstractions w.r.t. refinements, used for different analyses becomes easier, and can be properly ensured in a design methodology based on formal verification and synthesis methods.

Related works in this aim, and closer in spirit to our approach (to focus on modeling time) are domain-specific languages such as Prelude 11 to model the real-time characteristics of embedded software architectures. Conversely, standard architecture description languages could be based on algebraic modeling tools, such as interface theories with the ECDAR tool 12. Project TEA contributed a formal semantics of the AADL standard and the proposal of a time specification annex, using CCSL to model concurrency, time and physical properties, and PSL to model timed traces.

3.4 Scheduling Theory

Based on sound formalization of time and CPS architectures, real-time scheduling theory provides tools for predicting the timing behavior of a CPS which consists of many interacting software and hardware components. Expressing parallelism among software components is a crucial aspect of the design process of a CPS. It allows for efficient partition and exploitation of available resources.

The literature about real-time scheduling 13 provides very mature schedulability tests regarding many scheduling strategies, preemptive or non-preemptive scheduling, uniprocessor or multiprocessor scheduling, etc. Scheduling of data-flow graphs has also been extensively studied in the past decades.

A milestone in this prospect is the development of abstract affine scheduling techniques 14. It consists, first, of approximating task communication patterns (e.g. between Safety-Critical Java threads) using cyclo-static data-flow graphs and affine functions. Then, it uses state of the art ILP techniques to find optimal schedules and to concretize them as real-time schedules in the program implementations 1516.

Abstract scheduling, or the use of abstraction and refinement techniques in scheduling borrowed to the theory of abstract interpretation 17 is a promising development toward tooled methodologies to orchestrate thousands of heterogeneous hardware/software blocks on modern CPS architectures (just consider modern cars or aircrafts). It is an issue that simply defies the state of the art and known bounds of complexity theory in the field, and consequently requires a particular focus.

3.5 Verified programming for system design

The IoT is a network of devices that sense, actuate and change our immediate environment. Against this fundamental role of sensing and actuation, design of edge devices often considers actions and event timings to be primarily software implementation issues: programming models for IoT abstract even the most rudimentary information regarding timing, sensing and the effects of actuation. As a result, applications programming interfaces (API) for IoT allow wiring systems fast without any meaningful assertions about correctness, reliability or resilience.

We make the case that the "API glue" must give way to a logical interface expressed using contracts or refinement types. Interfaces can be governed by a calculus – a refinement type calculus – to enable reasoning on time, sensing and actuation, in a way that provides both deep specification refinement, for mechanized verification of requirements, and multi-layered abstraction, to support compositionality and scalability, from one end of the system to the other.

Our project seeks to elevate the “function as type” paradigm to that of “system as type”: to define a refinement type calculus based on concepts of contracts for reasoning on networked devices and integrate them as cyber-physical systems 18. An invited paper 19 outlines our progress with respect to this aim and plans towards building a verified programming environment for networked IoT devices: we propose a type-driven approach to verifying and building safe and secure IoT applications.

Accounting for such constrains in a more principled fashion demands reasoning about the composition of all the software and hardware components of the application. Our proposed framework takes a step in this direction by (1) using refinement types to make physical constraints explicit and (2) imposing an event-driven programming discipline to simplify the reasoning of system-wide properties to that of an event queue. In taking this approach, our approach would make it possible for a developer to build a verified IoT application by ensuring that a well-typed program cannot violate the physical constraints of its architecture and environment.

4.1 Automotive and Avionics

From our continuous collaboration with major academic and industrial partners through projects TOPCASED, OPENEMBEDD, SPACIFY, CESAR, OPEES, P and CORAIL, our experience has primarily focused on the aerospace domain. The topics of time and architecture of team TEA extend to both avionics and automotive. Yet, the research focuses on time in team TEA is central in any aspect of, cyber-physical, embedded system design in factory automation, automotive, music synthesis, signal processing, software radio, circuit and system on a chip design.

Multi-scale, multi-aspect time modeling, analysis and software synthesis will greatly contribute to architecture modeling in these domains, with applications to optimized (distributed, parallel, multi-core) code generation for avionics (project Corail with Thales avionics) as well as modeling standards, real-time simulation and virtual integration in automotive (project with Toyota ITC, section 8).

Together with the importance of open-source software, one of these projects, the FUI Project P (section 8), demonstrated that a centralized model for system design could not just be a domain-specific programming language, such as discrete Simulink data-flows or a synchronous language. Synchronous languages implement a fixed model of time using logical clocks that are abstraction of time as sensed by software. They correspond to a fixed viewpoint in system design, and in a fixed hardware location in the system, which is not adequate to our purpose and must be extended.

In project P, we first tried to define a centralized model for importing discrete-continuous models onto a simplified implementation of SIMULINK: P models. Certified code generators would then be developed from that format. Because this does not encompass all aspects being translated to P, the P meta-model is now being extended to architecture description concepts (of the AADL) in order to become better suited for the purpose of system design. Another example is the development of System modeler on top of SCADE, which uses the more model-engineering flavored formalism SysML to try to unambiguously represent architectures around SCADE modules.

An abstract specification formalism, capable of representing time, timing relations, with which heterogeneous models can be abstracted, from which programs can be synthesized, naturally appears better suited for the purpose of virtual prototyping. RT-Builder, based on the data-flow language Signal and developed by TNI, was industrially proven and deployed for that purpose at Peugeot. It served to develop the virtual platform simulating all on-board electronics of PSA cars. This `hardware in the loop” simulator was used to test equipments supplied by other manufacturers for virtual prototyping of cars. In the advent of the related automotive standard, RT-Builder then became AUTOSAR-Builder.

4.2 Factory Automation

In collaboration with Mitsubishi R&D, we explore another application domain where time and domain heterogeneity are prime concerns: factory automation. In factory automation alone, a system is conventionally built from generic computing modules: PLCs (Programmable Logic Controllers), connected to the environment with actuators and detectors, and linked to a distributed network. Each individual, physically distributed, PLC module must be timely programmed to perform individually coherent actions and fulfill the global physical, chemical, safety, power efficiency, performance and latency requirements of the whole production chain. Factory chains are subject to global and heterogeneous (physical, electronic, functional) requirements whose enforcement must be orchestrated for all individual components.

Model-based analysis in factory automation emerges from different scientific domains and focuses on different CPS abstractions that interact in subtle ways: logic of PLC programs, real-time electro-mechanical processing, physical and chemical environments. This yields domain communication problems that render individual domain analysis useless. For instance, if one domain analysis (e.g. software) modifies a system model in a way that violates assumptions made by another domain (e.g. chemistry) then the detection of its violation may well be impossible to explain to either the software or chemistry experts. As a consequence, cross-domain analysis issues are discovered very late during system integration and lead to costly fixes. This is particularly prevalent in multi-tier industries, such as avionic, automotive, factories, where systems are prominently integrated from independently-developed parts.

6.1 New software

7.1 A logical framework to verify requirements of hybrid system models

Participants: Jean-Pierre Talpin, Benoit Boyer, Stéphane Kastenbaum.

The goal of this PhD project is to build on the previous work done in Simon Lunel's PhD Thesis. The goal is to ensure the correctness-by-design of cyber-physical system models. The accent is put on developing a compositional contract framework that can help decomposing the systems into multiple sub-sytems easier to verify, leading to a proof of the global system.

We gained interest in the work of Benveniste et al. on multiple viewpoint contracts, and more particularly Pierluigi Nuzzo's PhD Thesis. It provides us a framework for decomposing systems into subsystems regardless of the formalism chosen to design it. In his Thesis, Pierliugi Nuzzo shows how this framework can also be used to show the compatibility of two subsystems designed in different formalism.

Another work that interested us is the framework developped by Naijun Zhan and its team at ISCAS. They worked on Hybrid Hoare Logic (HHL), Duration Calculus (DC) and Hybrid Communicating Sequential Process (HCSP). HCSP is a language to denote hybrid system, DC is a logic to describe traces of theses systems and HHL is a logic to show that DC traces corresponds to HCSP programs. They implemented all this components in MARS a software suite designed to translate Simulink systems into HCSP, and then prove some safety properties of the system with Isabelle. Our goal is to augment the MARS suite with a framework of multi-viewpoints contracts, implement it first in Isabelle/HOL, then plug it into MARS. This way, users will be able to design components in Simulink then export them with MARS into a collection of modular contracts and components. Which can be used to prove the safety of the system.

7.2 Semantic foundation for cyber-physical systems using higher-order UTP

Participants: Jean-Pierre Talpin, Xiong Xu, Naijun Zhan.

The arrival of Xiong with team TEA strenghtened our collaboration with Naijun Zhan's group at ISCAS.

We proposed a higher-order unifying theory of programming (HUTP) for the semantics foundation of cyber-physical systems (CPSs). It supports the specification of discrete, real-time and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we defined a calculus of hybrid designs to model, analyse, compose and refine heterogeneous CPSs. Some properties, such as deadlock, divergence, and non-termination, of hybrid designs were analysed algebraically. HUTP provides a uniform semantics domain capable of capturing all component models, at different abstraction levels, across heterogeneous domain concerns, into the same analysis framework.

Since there are natural links between hybrid designs and assume/guarantee contracts, we are trying to equip HUTP with compositional assume/guarantee reasoning and implement HUTP in Isabelle for automated verification. In addition, we wish to construct the HUTP semantics for the joint model AADL+Simulink/Stateflow and check the semantic equivalence between the informal data-flow model and its formal HCSP format within the HUTP framework.

We designed a higher-order extension of Hoare's UTP (Unified Theory of Programming) to modularly model hybrid and reactive systems. We demonstrated the expressiveness of the higher-order UTP (HUTP) by defining an encoding of two major logical frameworks for hybrid system design, namely the hybrid communicating sequential processes (HCSP) and hybrid programs with differential dynamic logic (dL). We introduced of a timed calculus of monadic refinement types based on an encoding of the duration calculus in HUTP to support contract-based reasoning using Dijkstra monads (in a similar manner as in the F* programming language). Finally, we started the development of higher-order UTP using the Isabelle/HOL theorem prover.

• “Semantic foundation for cyber-physical systems using higher-order UTP”. Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Naijun Zhan. Draft, submitted for publication, 20 pages, 2021.

7.3 Verified programming and secure integration of operating system libraries in F*

Participants: Shenghao Yuan, Jean-Pierre Talpin, Frédéric Besson.

The dynamics of Inria's challenge RIOT-fp accelerated with the arrival of Shenghao, which broadened to additional collaborations with teams Celtique (Frédéric Besson) and Prosecco (Denis Mérigoux).

The Ph.D. project of Shenghao is about formal verification and security properties of embedded operation system RIOT libraries. There are many approaches and languages to support formal methods, such as timed automata (UPPAAL), model-driven approaches (AADL and Synchronous Languages), proof systems (Coq and F*).

In this project, we focus on using the state-of-the-art theorem prover F* to model and verify the external libraries, because we will benefit a lot of F* features, for instance, strong type system, refinement type, precondition/postcondition proof style, and automatic theorem proof. We rely on the static analyzer infer to automatically generate some separation logic properties which are used to refine the F* model of the libraries. The safety and security of these libraries will be enforced by using the Steel compiler with the proof of safety and security strategies to perform C program transformations.

Currently, we have modelled the RIOT bootloader library in Low* (a subset of F*), the bootloader includes the fletcher32 algorithm and some ARM assembly code. The former is modelled in Low* because of the pointer type and some memory operations (e.g. memory copy), while the latter is too low-level. To solve that problem, we have formalized the syntax and semantics of the kernel ARM instruction set and planned to extend the vale project to support the ARM architecture for the F* verification framework.

In 2020, we implemented a verified implementation of RIOT’s bootloader that garantees the image integrity and the ARM assembly code that boots it, using F*'s Low* C code generator and by extending F*'s VALE framework to the verification of the ARM instructions of the bootloader responsible for jumping to the operating system's image.

• “Verified implementation of a secure bootloader using F* and VALE”. Shenghao Yuan, Jean-Pierre Talpin. Draft submitted for publication, 25 pages, 2021.

7.4 Abstract interpretation as a Dijkstra monad transformer

Participants: Lucas Franceschino, Jean-Pierre Talpin, David Pichardie.

This work aims at hybridizing abstract interpretation and weakest-preconditions, to enhance the programmer's experience working with certain kinds of dependently typed languages.

In such dependently typed language, the user is required to annotate terms with manual proofs or hints. While some automation facilities are provided by certain languages, i.e. to ease proofs, dependents types might be seen as requirements yielding proof obligations. On the other side, abstract interpretation is a sound theory of program approximation: an abstract interpreter gives rise to invariants by reading a source code.

These two theories are complementary: abstract interpretation sometimes produces invariants that one should have written explicitly as an annotation in its program. We particularly focus on bringing this hybridization to F*, by constructing a Dijkstra monad transformer.

This project aims at constructing an abstract interpreter along with a theorem of soundness, directly in F*. Most of the state of the art's abstract interpreter formalizations are written in Coq; in contrast, choosing F* makes our proof much lighter, thus our implementation is more concise. F* syntax is close to OCaml, and thus extracts to OCaml more or less transparently.

In collaboration with team Celtique, Lucas finalized the proof of soundness of Dijkstra monad transformer for hybridizing a (deductive) weakest pre-condition calculus with an abstract interpreter (for inferring pre- and post-conditions). This work lays the foundation for integrating abstract interpretations directly within F*'s dependent-type system to facilitate automated annotation and verification of programs:

• “Abstract interpretation as a Dijkstra monad transformer for low-level verification ”. Lucas Franceschino, Jean-Pierre Talpin, David Pichardie. Draft submitted for publication, 25 pages, 2021.

7.5 Verified information flow of embedded programs

Participants: Jean-Joseph Marty, Lucas Franceschino, Niki Vazou, Jean-Pierre Talpin.

This PhD project is about applying refinement types theory to verified programming of applications and modules of library operating systems, such as unikernels, for embedded devices of the Internet of Things (IoT): TinyOS, Riot, etc. Our topic has focused on developing a model of information flow control using labeled input-outputs (LIO) implemented using F$☆$: project Lio$☆$.

As part of the development of Lio$☆$, we implemented a library that, thanks to static verification, ensures the containment of information in relation to a parameterized policy for information flow control. In collaboration with Niki Vazou (IMDEA) and Lucas Franceschino we have formalized and developed an automatic method to prove non-interference in Meta$☆$. Using the Kremlin code generator, programs using Lio$☆$ can be compiled into C code and run natively on embedded low-resource-constrained devices, without the need for additional runtime system. We completed a layered implementation of the LIO framework for information flow control of embedded applications developped with the Low* code generator and submitted our results to an A* conference:

• “LIO*: Information Flow Control for IoT devices with F*”. Jean-Joseph Marty, Lucas Francechino, Jean-Pierre Talpin, Niki Vazou. Draft submission, 20 pages, 2020. An earlier version is available on arxiv.org

In parallel we continued our collaboration with the ProgSys team on a second, now discontinued, project: Gluco$☆$. The goal of this project was to evaluate the capabilities to use the F* programming language to program an entire system by taking into account its software, hardware and physical constraints using type refinements 20.

7.6 The polychronous model, its incarnation language Signal and its open-source software toolset Polychrony

Participants: Loïc Besnard, Thierry Gautier.

We have recently compared the model of asynchronous dataflow represented by Kahn Process Networks and that of synchronous dataflow represented by the polychronous model (a paper is still in review process). In line with our old and recent work on the polychronous model, we have produced a new version of the Signal language reference manual 13. The previous version was about ten years old. Among the main changes made in this new version, we can note the addition of new classes of process models with in particular the automaton models, the addition of guarded processes (that may be compared, for instance, to “clocked guarded actions” that exist in some formalisms), a new definition of the tick of a process, and the addition of specific “pragmas” (pragmas allow to associate specific information that will be used by a given compiler or another tool). At the same time, we finalized a new version of the open-source software Polychrony, released online in December 2020 (http://polychrony.inria.fr). The development of this new version is now managed under git. It integrates the latest functionalities developed in the Signal compiler, in particular a code generation technique for so-called “polyendochronous processes” (which may be seen as particular networks of processes exhibiting polyhierarchies of clocks). New compiler options have been created for the new features and all previously available options have been reviewed (they are described in the online help obtained by the “signal -h” command).

7.7 ADFG: Affine data-flow graphs scheduler synthesis

Participants: Loïc Besnard, Thierry Gautier, Jean-Pierre Talpin, Shuvra Bhattacharyya, Alexandre Honorat, Hai Nam Tran.

We continued our research involving the development of advanced signal processing dataflow methods for the ADFG tool. This research is collaboratively developed with the TEA Team, Hai Nam Tran (Lab-STICC/UBO), Alexandre Honorat (INSA) and Shuvra Bhattacharyya (UMD/INSA/INRIA). Emphasis during this reporting period has been on the development of a framework to integrate the scheduling synthesized by ADFG into a scheduling simulator and a code generator targeting the RTEMS (Real-Time Executive for Multiprocessor Systems) RTOS https://www.rtems.org.

8.1 Bilateral contracts with industry

Inria – Mitsubishi Electric framework program (2018+)

• Title: Inria – Mitsubishi Electric framework program
• INRIA principal investigator: Jean-Pierre Talpin
• International Partner: Mitsubishi Electric R&D Europe (MERCE)
• Duration: 2018+
• Abstract: Following up the fruitful collaboration of TEA with the formal methods group at MERCE, Inria and Mitsubishi Electric signed an Inria-wide collaboration agreement, which currently hosts projects with project-teams Sumo and Tea, as well as Tocata.

8.2 Bilateral grants with industry

Mitsubishi Electric R&D Europe (2019-2022)

• Title: A logical framework to verify requirements of hybrid system models
• INRIA principal investigator: Jean-Pierre Talpin, Stéphane Kastenbaum
• International Partner: Mitsubishi Electric R&D Europe
• Duration: 2015 - 2018
• Abstract: The goal of this doctoral project is to verify and build cyber-physical systems (CPSs) with a correct-by-construction approach in order to validate system requirements against the two facets of the cyber and physical aspects of such designs. Our approach is based on components augmented with formal contracts that can be composed, abstracted or refined. It fosters on the proof of system-level requirements by composing individual properties proved at component level. While semantically grounded, the tooling of this methodology should be usable by regular engineers (i.e. not proof theory specialists).

9.1 International initiatives

9.2 National initiatives

General chair, scientific chair

Jean-Pierre Talpin serves the steering committee of the ACM-IEEE MEMOCODE conference since 2003, of which he was nominated Chair for three years in 2021.

Member of the conference program committees

Jean-Pierre Talpin participated to the program committees of ACM LCTES'20, ACM SAC'20, SCOPES'20, SAMOS'20.

Member of the editorial boards

Jean-Pierre Talpin served the ACM Transactions on Embedded Computing Systems (TECS) from 2013 to 2020 under the Chief Editorship of Sandeep Kumar Shukla.

10.1 Teaching - Supervision - Juries

Jean-Pierre Talpin served as “rapporteur” at the PhD Thesis defense of Guillaume Dupont, entitled “Correct-by-Construction Design of Hybrid Systems Based on Refinement and Proof”.

10.2 Popularization

We published an article on Inria blog “Emergence” presenting the topic of our collaboration with Mitsubishi Electric (MERCE) in the PhD project of Stéphane Kastenbaum, and on the occasion of the recently signed Inria-MERCE framework program, that additionally hosts collaborations with teams Sumo and Toccata.

11.1 Major publications

• 1 incollection LoicL. Besnard, ThierryT. Gautier, PaulP. Le Guernic, ClémentC. Guy, Jean-PierreJ.-P. Talpin, BrianB. Larson and EtienneE. Borde. Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard Cyber-Physical System Design from an Architecture Analysis Viewpoint Cyber-Physical System Design from an Architecture Analysis Viewpoint Springer January 2017
  HAL DOI
• 2 incollectionLoïcL. Besnard, ThierryT. Gautier, PaulP. Le Guernic and Jean-PierreJ.-P. Talpin. Compilation of Polychronous Data Flow EquationsSynthesis of Embedded SoftwareSpringer2010, 1-40
  HALDOI
• 3 inproceedingsAdnanA. Bouakaz and Jean-PierreJ.-P. Talpin. Design of Safety-Critical Java Level 1 Applications Using Affine Abstract ClocksInternational Workshop on Software and Compilers for Embedded SystemsSt. Goar, GermanyJune 2013, 58-67
  HALDOI
• 4 articleAbdoulayeA. Gamatié, ThierryT. Gautier and PaulP. Le Guernic. Synchronous design of avionic applications based on model refinementsJournal of Embedded Computing (IOS Press)23-42006, 273-289
  HAL
• 5 inproceedingsAlexandreA. Honorat, Hai NamH. Tran, LoïcL. Besnard, ThierryT. Gautier, Jean-PierreJ.-P. Talpin and AdnanA. Bouakaz. ADFG: a scheduling synthesis tool for dataflow graphs in real-time systemsInternational Conference on Real-Time Networks and Systems Grenoble, FranceOctober 2017, 1-10
  HALDOI
• 6 inproceedings SimonS. Lunel, BenoîtB. Boyer and Jean-PierreJ.-P. Talpin. Compositional proofs in differential dynamic logic dL 17th International Conference on Application of Concurrency to System Design Zaragoza, Spain June 2017
  HAL
• 7 inproceedingsSimonS. Lunel, StefanS. Mitsch, BenoîtB. Boyer and Jean-PierreJ.-P. Talpin. Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic LogicFM 2019 - 23rd International Symposium on Formal MethodsLong version of an article accepted to the conference FM'19Porto, PortugalOctober 2019, 1-22
  HAL
• 8 book ShinS. Nakajima, Jean-PierreJ.-P. Talpin, MasumoM. Toyoshima and HuafengH. Yu. Cyber-Physical System Design from an Architecture Analysis Viewpoint Communications of NII Shonan Meetings Springer January 2017
  HAL DOI
• 9 techreportVirginiaV. Papailiopoulou, DumitruD. Potop-Butucaru, YvesY. Sorel, RobertR. De Simone, LoicL. Besnard and Jean-PierreJ.-P. Talpin. From concurrent multi-clock programs to concurrent multi-threaded implementationsRR-7577INRIAMarch 2011, 22
  HAL
• 10 inproceedingsOcanO. Sankur and Jean-PierreJ.-P. Talpin. An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)10206Lecture Notes in Computer ScienceUppsala, SwedenSpringer Berlin HeidelbergApril 2017, 23-40
  HAL
• 11 inproceedings HuafengH. Yu, JoshiJ. Prashi, Jean-PierreJ.-P. Talpin, Sandeep KumarS. Shukla and Shin'IchiS. Shiraishi. Model-Based Integration for Automotive Control Software Digital Automation Conference ACM San Francisco, United States June 2015
  HAL

11.2 Publications of the year