6.1.1 pyCPA_TWCA

• Name: Analysis tool for weakly-hard real-time systems
• Keywords: Real time, Scheduling analyses
• Functional Description: pyCPA_TWCA is a pyCPA plugin for Typical Worst-Case Analysis. pyCPA is an open-source Python implementation of Compositional Performance Analysis developed at TU Braunschweig, which allows in particular response-time analysis. pyCPA_TWCA is an extension of that tool that is co-developed by Sophie Quinton and Zain Hammadeh at TU Braunschweig. It allows in particular the computation of weakly-hard guarantees for real-time tasks, i.e. number of deadline misses out of a sequence of executions. So far, pyCPA_TWCA is restricted to uniprocessor systems of independent tasks. pyCPA_TWCA can handle the following scheduling policies: Fixed Priority Preemptive, Fixed Priority Non-Preemptive, Weighted Round-Robin, Earliest Deadline First.
• Contact: Sophie Quinton

6.1.2 CertiCAN

• Name: Certifier of CAN bus analysis results
• Keywords: Certification, CAN bus, Real time, Static analysis
• Functional Description: CertiCAN is a tool, produced using the Coq proof assistant, allowing the formal certification of the correctness of CAN bus analysis results. Result certification is a process that is light-weight and flexible compared to tool certification, which makes it a practical choice for industrial purposes. The analysis underlying CertiCAN, which is based on a combined use of two well-known CAN analysis techniques, is computationally efficient. Experiments demonstrate that CertiCAN is able to certify the results of RTaW-Pegase, an industrial CAN analysis tool, even for large systems. Furthermore, CertiCAN can certify the results of any other RTA tool for the same analysis and system model (periodic tasks with offsets in transactions).
• Contacts: Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton

7.1.1 Hypercells

The Hypercell framework, presented in  52, allows the definition of different component models for dynamic software architectures featuring both sharing and encapsulation. Its behavioral theory is still in its initial stages but features the definition of a form of contextual bisimilarity. This year has seen the further development of the framework with new results on the modeling of encapsulation policies and their characterization by means of contextual bisimilarity, and the development of a first implentation of the framework as a Rust programming language library.

In collaboration with the Spirals team at Inria Lille – Nord Europe, and Orange, we have used hypercells as a pivot model for developing interpretations, formally defined with the Alloy specification language, of various languages and formalisms for the description of software configurations for cloud computing environments. Configuration languages considered include the TOSCA and OCCI standards, as well as the Open Stack Heat Orchestration Template (HOT), Docker Compose, and the Aeolus component model for cloud deployment. This work, developed as part of a bilateral contract with Orange, allowed the development of a verification tool for the correctness of HOT configurations, helped uncover several flaws in the HOT specifications, and in the ETSI NFV standard. The work is reported in 20.

7.1.2 Dynamicity in dataflow models

Recent dataflow programming environments support applications whose behavior is characterized by dynamic variations in resource requirements. The high expressive power of the underlying models (e.g., Kahn Process Networks or the CAL actor language) makes it challenging to ensure predictable behavior. In particular, checking liveness (i.e., no part of the system will deadlock) and boundedness (i.e., the system can be executed in finite memory) is known to be hard or even undecidable for such models. This situation is troublesome for the design of high-quality embedded systems. In the past few years, we have proposed several parametric dataflow models of computation (MoCs)  37, 28, we have written a survey providing a comprehensive description of the existing parametric dataflow MoCs  31, and we have studied symbolic analyses of dataflow graphs  32. More recently, we have proposed an original method to deal with lossy communication channels in dataflow graphs  35.

We are nowadays studying models allowing dynamic reconfigurations of the topology of the dataflow graphs. This is required by many modern streaming applications that have a strong need for reconfigurability, for instance to accommodate changes in the input data, the control objectives, or the environment.

We have proposed a new MoC called Reconfigurable Dataflow (RDF)  36. RDF extends SDF with transformation rules that specify how the topology and actors of the graph may be reconfigured. Starting from an initial RDF graph and a set of transformation rules, an arbitrary number of new RDF graphs can be generated at runtime. Transformations can be seen as graph rewriting rules that match some sub-part of the dataflow graph and replace it by another one. Transformations can be applied an arbitrary number of times during execution and therefore can produce an arbitrary number of new graphs. The major feature and advantage of RDF is that it can be statically analyzed to guarantee that all possible graphs generated at runtime will be connected, consistent, and live. To the best of our knowledge, RDF is the only dataflow MoC allowing an arbitrary number of topological reconfigurations while remaining statically analyzable. The RDF MoC has been implemented by Arash Shafiei within a software tool that allows the designer to write an initial RDF graph and its transformation rules. The static analyses for connectivity, consistency, and liveness have been implemented too. And a canny edge detector case study shows that dynamic reconfigurations to increase the parallelism level, when the incoming video stream becomes more computationally intensive, can be performed seamlessly. Finally, we have proposed in 2020 a new latency analysis for RDF that allows us to bound the latendy variation incurred by applying a given transformation rule whatever the RDF graph it is applied to.

This is the research topic of Arash Shafiei's PhD, in collaboration with Orange Labs.

7.2.1 A Markov Decision Process approach for energy minimization policies

In the context of independent real-time sporadic jobs running on a single-core processor equipped with Dynamic Voltage and Frequency Scaling (DVFS), we have proposed a Markov Decision Process approach (MDP) to minimize the energy consumption while guaranteeing that each job meets its deadline. The idea is to leverage on the statistical information on the jobs' characteristics available at design time: release time, worst-case execution time (WCET), and relative deadline. This is the topic of Stephan Plassart's PhD 18, funded by the Caserm Persyval project. We have considered several cases depending on the amount of information available at design time:

• Offline case: In the offline case, all the information is known and we have proposed the first linear complexity offline scheduling algorithm that minimizes the total energy consumption 9, 19: our complexity is $𝒪\left(n\right)$, where $n$ is the number of jobs to be scheduled, while the previously best known algorithms were in $𝒪\left(n^2\right)$ and $𝒪(nlogn)$  47.
• Clairvoyant case: In the clairvoyant case, the characteristics of the jobs are only known statistically, and each job's WCET and relative deadline are only known at release time. We want to compute the optimal online scheduling speed policy that minimizes the expected energy consumption while guaranteeing that each job meets its deadline. This general constrained optimization problem can be modeled as an unconstrained MDP by choosing a proper state space that also encodes the constraints of the problem. In the finite horizon case we use a dynamic programming algorithm, while in the infinite horizon case we use a value iteration algorithm 10.
• Non-clairvoyant case: In the non-clairvoyant case, the actual execution time (AET) of a job is only known only when this job completes its execution. This AET is of course assumed to be less than the WCET, which is known at the job's release time. Again, by building an MDP for the system with a well chosen state, we compute the optimal online scheduling speed policy that minimizes the expected energy consumption 16.
• Learning case: In the learning case, the only information known for the jobs are a bound on the jobs' WCETs and a bound on their deadlines. We have proposed two reinforcement learning algorithms, one that learns the optimal value of the expected energy (Q-learning), and another one that learns the probability transition matrix of the system, from which we derive the optimal online speed policy.

This work led us to compare several existing speed policies with respect to their feasibility. Indeed, the policies (OA)  54, (AVR)  54, and (BKP)  26 all assume that the maximal speed $S_{max}$ available on the processor is infinite, which is an unrealistic assumption. For these three policies and for our (MDP) policy, we have established necessary and sufficient conditions on $S_{max}$ guaranteeing that no job will ever miss its deadline 11.

7.2.2 Formal proofs for schedulability analysis of real-time systems

We contribute to Prosa 21, a Coq library of reusable concepts and proofs for real-time systems analysis. A key scientific challenge is to achieve a modular structure of proofs, e.g., for response time analysis. Our goal is to use this library for:

1. a better understanding of the role played by some assumptions in existing proofs;
2. a formal verification and comparison of different analysis techniques; and

3. the certification of results of existing (e.g., industrial) analysis tools.

We advanced our work on formal proofs for schedulability analysis of real-time systems mainly in two directions in 2020. First, several optimizations have increased dramatically the timing efficiency of our CertiCAN tool, the first formally proven tool able to certify the results of commercial CAN analysis tools. This work is included in the PhD thesis of Xiaojie Guo (not yet published), who defended in December 2020. Second, Paolo Torrini, who was recruited in July 2020, has opened a new line of work on correct by construction implementation of schedulers.

7.2.3 Scheduling under multiple constraints and Pareto optimization

We have considered the bi-criteria minimization problem in the (worst-case execution time – WCET, worst-case energy consumption – WCEC) space for real-time programs. To the best of our knowledge, this is the first contribution of this kind in the literature.

A real-time program is abstracted as a Timed Control Flow Graph (TCFG), where each basic block is labeled with the number of clock cycles required to execute it on the chosen processor at the nominal frequency. This timing information can be obtained, for instance, with a WCET analysis tool. The target processor is equipped with dynamic voltage and frequency scaling (DVFS) and offers several (frequency $f$, voltage $V$) operating points, as is the case with most processors today. The goal is to compute a set of assignments from the set of basic blocks of the TCFG to the set of available $(f,V)$ pairs, such that each such assignment is a non-dominated points in the (WCET, WCEC) plane, non-dominated in the Pareto sense.

From the TCFG we extract the longest execution path, and then we compute the WCET and the WCEC for this path at a chosen $(f,V)$ pair. By construction, all the other execution paths are shorter, so this WCET and this WCEC hold for the whole program. This ensures that each single-frequency assignment is a non-dominated point, and therefore belongs to the Pareto front. Then, we have studied two frequencies assignments, still for the longest execution path. When the frequency switching costs in time and in energy are assumed to be negligible, we have proved that each two frequencies (say with $f_i$ and $f_k$) assignment is a point located in the segment between the single frequency assignment at $f_i$ and the single frequency assignment at $f_k$. We have also proposed a linear time heuristic to assign a $(f,V)$ pair to all the other blocks (i.e., those not belonging to the longest path) such that all the other execution paths of the TCFG have a shorter WCET and a lesser WCEC. We have also established conditions under which the resulting assignment corresponds to a non-dominated point. Finally, we have generalized these results to the case where the frequency switching costs are not negligible. Surprisingly, this case reduces the size of the search space from exponential ($m^n$, where $n$ is the number of blocks and $m$ is the number of frequencies) to polynomial because all the assignments involving more than three different frequencies will be dominated by an assignment involing either one or two frequencies. This key result allows us to generate the exact Pareto front. This was the topic of Jia Jie Wang's postdoc.

All our algorithms have been evaluated on a set of hard real time benchmark programs. This shows that they perform extremely well. Our DVFS assignment algorithm can also be used as a back-end for the compiler of the Pret-C programming language  22, 23, 1 in order to make it energy aware, thanks to the ability of this compiler to generate TCFGs. Future work will invlove developping similar algorithms but in the much more difficult case of the parallel programming language ForeC  39.

7.3.1 Fault Ascription in Concurrent Systems

Fault ascription is a precise form of fault diagnosis that relies on counterfactual analysis for pinpointing the causes of system failures. Research on counterfactual causality has been marked, until today, by a succession of definitions of causation that are informally validated against human intuition on mostly simple examples. This approach suffers from its dependence on the tiny number and incompleteness of examples in the literature, and from the lack of objective correctness criteria  41.

We have introduced in 14 a general framework for fault ascription, which consists in identifying, in a concurrent system, the events or components whose faulty behavior has caused the failure of said system. Our framework uses configuration structures as a general semantical model to handle truly concurrent executions, partial and distributed observations in a uniform way. In contrast with most of the current literature on counterfactual analysis which relies heavily on a set of toy examples, we have defined a set of expected formal properties for counterfactual builders, i.e. operators that build counterfactual executions. We have then shown that causality analyses that satisfy our requirements meet a set of elementary soundness and completeness properties. Finally we have presented a concrete causality analysis meeting all our requirements, and we have shown it to be monotonic under two forms of refinement.

7.3.2 Causal Explanations for Embdded Systems

Model-Based Diagnosis of discrete event systems (DES) usually aims at detecting failures and isolating faulty event occurrences based on a behavioural model of the system and an observable execution log. The strength of a diagnostic process is to determine what happened that is consistent with the observations. In order to go a step further and explain why the observed outcome occurred, we borrow techniques from causal analysis. We are currently exploring techniques that are able to extract, from an execution trace, the causally relevant part for a property violation. As part of the SEC project we are investigating how such techniques can be extended to classes of real-time systems.

7.3.3 Fault Management in Virtualized Networks

From a more applied point of view we have been investigating approaches for fault explanation and localization in virtualized networks. In essence, Network Function Virtualization (NFV), widely adopted by the industry and the standardization bodies, is about running network functions as software workloads on commodity hardware to optimize deployment costs and simplify the life-cycle management of network functions. However, it introduces new fault management challenges including dynamic topology and multi-tenant fault isolation. In her PhD thesis 17, Sihem Cherrared has proposed a model-based root cause analysis framework for virtualized networks. In order to overcome the lack of accurate previous knowledge, the framework features a self-modeling algorithm that models the dependencies within and between layers of virtual networks, including auto-recovery and elasticity aspects. Model-based diagnosis is performed using constraint solving on the previous and acquired knowledge.

9.1.1 ANR

9.1.2 Institute of Technology (IRT)

SEC

Participants: Gregor Goessler, Thomas Mari.

SEC (Safe and Explainable Cyber-physical systems, 2019–22) is a joint project by Spades and Verimag, funded by the "Initiative of Excellence" of Grenoble University. It funds Thomas Mari's PhD thesis.

10.1.1 Scientific events: organisation

10.1.2 Scientific events: selection

10.1.3 Journal

10.1.4 Leadership within the scientific community

• Alain Girault is a member of the EMSIG board and he manages its mailing list.
• Sophie Quinton is a member of the ACM SIGBED Executive Committee and Associate Editor of the SIGBED Blog.
• Sophie Quinton co-chairs a working group of the GDR CIS associated with the Center for Internet and Society (http://cis.cnrs.fr/) focused on environmental issues.

10.1.5 Scientific expertise

• Gregor Gössler has reviewed a project for the French funding agency ANR.

10.1.6 Research administration

• Pascal Fradet is head of the committee for doctoral studies (“Responsable du comité des études doctorales”) of the Inria Grenoble – Rhône-Alpes research center and local correspondent for the young researchers Inria mission (“Mission jeunes chercheurs”).
• Alain Girault is Deputy Scientific Director in charge of the domain “Algorithmics, Programming, Software and Architecture”.
• Xavier Nicollin is member of the committee for computing resources users (“Comité des Utilisateurs des Moyens Informatiques”) of the Inria Grenoble – Rhône-Alpes research center.
• Sophie Quinton is in charge of organizing discussions and actions regarding the environmental and societal impact of our research at Inria Grenoble Rhône-Alpes.
• Jean-Bernard Stefani is Head of Science of the Inria Grenoble Rhône-Alpes research center.

10.2.1 Teaching

• Licence : Pascal Fradet, Théorie des Langages 1 & 2, 36 HeqTD, niveau L3, Grenoble INP (Ensimag), France
• Licence : Pascal Fradet, Modèles de Calcul : $\lambda$-calcul, 12 HeqTD, niveau L3, Univ. Grenoble Alpes, France
• Master : Xavier Nicollin, Analyse de Code pour la Sûreté et la Sécurité, 45 HeqTD, niveau M1, Grenoble INP (Ensimag), France
• Licence : Xavier Nicollin, Théorie des Langages 1, 48 HeqTD, niveau L3. Grenoble INP (Ensimag), France
• Licence : Xavier Nicollin, Théorie des Langages 2, 37,5 HeqTD, niveau L3, Grenoble INP (Ensimag), France
• Licence : Xavier Nicollin, Bases de la Programmation Impérative, 30 HeqTD, niveau L3, Grenoble INP (Ensimag), France
• Master : Sophie Quinton, Performance and Quantitative Properties, 8 HeqTD, MOSIG, Univ. Grenoble Alpes, France
• Master: Jean-Bernard Stefani, Formal Aspects of Component Software, 9h, MOSIG, Univ. Grenoble Alpes, France.

10.2.2 Supervision

• PhD: Sihem Cherrared, “Fault Management in Multi-Tenant Programmable Networks”; Univ. Rennes 1; defended on June 26, 2020; co-advised by Eric Fabre and Gregor Gössler.
• PhD in progress: Thomas Mari, “Construction of Safe Explainable Cyber-physical systems”; Grenoble INP; since October 2019; co-advised by Gregor Gössler and Thao Dang.
• PhD defended in June 2020: Stephan Plassart, “On-line optimization in dynamic real-time systems”; Univ. Grenoble Alpes; co-advised by Bruno Gaujal and Alain Girault.
• PhD defended on December 18 2020: Xiaojie Guo, “Formal Proofs for the Analysis of Real-Time Systems in Coq”; Univ. Grenoble Alpes; since December 2016; co-advised by Pascal Fradet, Jean-François Monin, and Sophie Quinton.
• PhD in progress: Maxime Lesourd, “Generic Proofs for the Analysis of Real-Time Systems in Coq”; Univ. Grenoble Alpes; since September 2017; co-advised by Pascal Fradet, Jean-François Monin, and Sophie Quinton.
• PhD in progress: Arash Shafiei, “RDF: A reconfigurable dataflow MoC supporting dynamic topological transformations and static analyzability”; Univ. Grenoble Alpes; since September 2017; co-advised by Pascal Fradet, Alain Girault, and Xavier Nicollin.
• PhD in progress: Martin Vassor, “Analysis and types for safe dynamic software reconfigurations”; Univ. Grenoble Alpes; since November 2017; co-advised by Pascal Fradet and Jean-Bernard Stefani.

10.2.3 Juries

• Alain Girault was president of the PhD jury of Alexandre Honorat (INSA-Rennes).
• Gregor Gössler was reviewer for the PhD thesis of Valentin Bouziat (Toulouse University).

10.3.1 Education

• Sophie Quinton is part of the scientific committee of the upcoming “COP2 étudiante” (https://cop2etudiante.org/).

10.3.2 Interventions

• Sophie Quinton was invited to the panel of Forum 5i on the topic: “Innovation and carbon footprint: which synergies ?”.

International journals

• 9 article BrunoB. Gaujal, AlainA. Girault and StéphanS. Plassart. A Pseudo-Linear Time Algorithm for the Optimal Discrete Speed Minimizing Energy Consumption Discrete Event Dynamic Systems 2020
  HAL back to text
• 10 articleBrunoB. Gaujal, AlainA. Girault and StéphanS. Plassart. Dynamic Speed Scaling Minimizing Expected Energy Consumption for Real-Time TasksJournal of SchedulingJuly 2020, 1-25
  HALDOIback to text
• 11 article BrunoB. Gaujal, AlainA. Girault and StéphanS. Plassart. Feasibility of on-line speed policies in real-time systems Real-Time Systems April 2020
  HAL DOI back to text
• 12 articleKai-BjörnK.-B. Gemlau, LeonieL. Köhler, RolfR. Ernst and SophieS. Quinton. System-level Logical Execution Time: Augmenting the Logical Execution Time Paradigm for Distributed Real-Time Automotive SoftwareACM Transactions on Cyber-Physical Systems52January 2021, 1-27
  HALDOI
• 13 articleAntoineA. Girard and GregorG. Gössler. Safety Synthesis for Incrementally Stable Switched Systems using Discretization-Free Multi-Resolution AbstractionsActa Informatica572020, 245-269
  HALDOI
• 14 articleGregorG. Gössler and Jean-BernardJ.-B. Stefani. Causality analysis and fault ascription in component-based systemsTheoretical Computer Science8372020, 158-180
  HALDOIback to text
• 15 articleZain A HZ. Hammadeh, SophieS. Quinton and RolfR. Ernst. Weakly-hard Real-time Guarantees for Earliest Deadline First Scheduling of Independent TasksACM Transactions on Embedded Computing Systems (TECS)186January 2020, 1-25
  HALDOI

Conferences without proceedings

• 16 inproceedingsBrunoB. Gaujal, AlainA. Girault and StéphanS. Plassart. Discrete and Continuous Optimal Control for Energy Minimization in Real-Time SystemsEBCCSP 2020 - 6th International Conference on Event-Based Control, Communication, and Signal ProcessingKrakow, PolandSeptember 2020, 1-8
  HALback to text

Doctoral dissertations and habilitation theses

• 17 thesis SihemS. Cherrared. Fault management of programmable multi-tenant networks Université Rennes 1 June 2020
  HAL back to text
• 18 thesis StéphanS. Plassart. Online optimization in dynamic real-time systems Université Grenoble Alpes [2020-....] June 2020
  HAL back to text

Reports & preprints

• 19 report BrunoB. Gaujal, AlainA. Girault and StéphanS. Plassart. A Linear Time Algorithm Computing the Optimal Speeds Minimizing Energy Under Real-Time Constraints Inria Grenoble Rhône-Alpes April 2020
  HAL back to text
• 20 report PhilippeP. Merle, SouhaS. Ben Rayana, LionelL. Seinturier, RogerR. Pissard-Gibollet, Jean-BernardJ.-B. Stefani and AdjaA. Ndeye Sylla. Towards a formal reference computational model for cloud configuration management INRIA January 2020
  HAL back to text