Publications of Sophie Quinton

2024

Conference papers

titre

Taking conviviality seriously (extended abstract)

auteur

Sophie Quinton, Jean-Bernard Stefani

resume

In his seminal book, “Tools for conviviality”, Ivan Illich laid down a strikingly prescient analysis of the woes that can plague a technological society. Illich’s ideas around convivial tools seem nowadays to resonate well within the computer science and engineering community. We believe that taking Illich’s conviviality seriously could provide a useful starting point for discussion and collaboration between computing and science and technology scholars.

Accès au texte intégral et bibtex

titre

Informatique et durabilité, une difficile transposition didactique

auteur

Baptiste de Goër, Hersch Micha, Sophie Quinton

resume

Dans le contexte actuel de changement climatique, une demande forte d’enseigner à l’école les enjeux de durabilité liés au numérique émerge dans la société et en provenance des institutions. Or, la transposition didactique de ces sujets dans les cours d’informatique soulève un certain nombre de difficultés. Ce papier présente dans un premier temps un aperçu des savoirs scientifiques sur le sujet, des pratiques académiques associées et met en avant la difficile articulation entre l’informatique comme discipline scientifique et les questions de durabilité. Dans un second temps, inspirés de réflexions issues de l’éthique de la technologie, nous évoquons la possibilité de réancrer l’informatique dans le contexte matériel, économique, social et politique de son développement et de ses applications, ce qui constituerait une évolution importante de l’informatique aussi bien au niveau scolaire qu’académique.

Accès au texte intégral et bibtex

titre

Informatique et durabilité, une difficile transposition didactique

auteur

Baptiste de Goër, Micha Hersch, Sophie Quinton

resume

Dans le contexte actuel de changement climatique, une demande forte d’enseigner à l’école les enjeux de durabilité liés au numérique émerge de la société et des institutions. Or, la transposition didactique de ces sujets dans les cours d’informatique soulève un certain nombre de difficultés. Dans un premier temps, ce papier présente un aperçu des savoirs scientifiques sur la question et des pratiques d’enseignement académique associées, puis met en avant la difficile articulation entre l’informatique comme discipline scientifique et les questions de durabilité. Dans un second temps, inspirés de réflexions issues de l’éthique de la technologie, nous évoquons la possibilité de réancrer l’informatique dans le contexte économique, social, politique, mais également matériel, de son développement et de ses applications ; ce qui constituerait une évolution importante de l’informatique aussi bien au niveau scolaire qu’académique.

Accès au texte intégral et bibtex

2023

Journal articles

titre

A long road ahead: a review of the state of knowledge of the environmental effects of digitization

auteur

Gauthier Roussilhe, Anne-Laure Ligozat, Sophie Quinton

resume

In this brief review, we report on the state of knowledge and its limitations regarding the environmental footprint of the digital sector. While the final energy consumption and the related carbon footprint of information and communication technologies (ICT) are well studied, other environmental factors and some phases of the life cycle are still poorly understood. New connected equipment and services currently being deployed make such assessments even more complex. In addition, more research is needed on the indirect effects of ICT (i.e. substitution, optimization and various rebound effects). Indeed, recent reports tend to ignore or minimize the negative effects of digitization. Because indirect effects depend on external factors such as regulations, prices, socio-cultural contexts, etc., extrapolations are extremely uncertain. Methodological elements have been proposed to perform such evaluations, but there is still a long way to go.

DOI

DOI : 10.1016/j.cosust.2023.101296

Accès au texte intégral et bibtex

Conference papers

titre

Assessing the Potential of Carpooling for Reducing Vehicle Kilometers Traveled

auteur

Aina Rasoldier, Alain Girault, Sophie Quinton, Jacques Combaz, Kevin Marquet

resume

The national and local strategies implemented to achieve the French Nationally Determined Contribution (a key element of the Paris Agreement) rely heavily on technological improvements to reach carbon neutrality by 2050, which raises the question of whether these technologies can rise to the challenge, and which social changes are needed to make these technologies reach their full potential. One example of this is the use of digital platforms for developing carpooling. We study the maximum potential of two carpooling schemes for local travel. Our results show that a massive adoption of carpooling would be needed to reach targets set by the national and local strategies, even under maximizing assumptions.

DOI

DOI : 10.1109/ICT4S58814.2023.00021

Accès au texte intégral et bibtex

2022

Journal articles

titre

The crisis of the scientific mind : an investigation, a tragedy and a collective redistribution of roles

auteur

Eric Tannier, Vincent Daubin, Sophie Quinton

resume

The process of scientific research resembles that of an investigator : observations, hypotheses, verifications, conclusions. In the case of ecological devastation, our community describes the state and dynamics of the contemporary world, tries to understand the causes in order to better propose means of action. But as is often the case for investigators, the possibility of their own responsibility is not often considered. For this, it is necessary to undertake a reflexive observation of one’s own functioning, and of the relationships that one weaves with the dynamics of the world. We report on the setting up of a possible instrument for this reflexivity, and how collective discussion makes it possible to find ways for scientists, at all organisational levels, to exercise their environmental responsibility.

DOI

DOI : 10.4000/framespa.13150

Accès au texte intégral et bibtex

Conference papers

titre

A Formal Link Between Response Time Analysis and Network Calculus

auteur

Pierre Roux, Sophie Quinton, Marc Boyer

resume

Classical Response Time Analysis (RTA) and Network Calculus (NC) are two major formalisms used for the verification of real-time properties. We offer mathematical links between these two different theories. Based on these links, we then prove the equivalence of various key notions in both frameworks. This enables specialists of both formalisms to get increase confidence on their models, or even, like the authors, to discover errors in theorems by investigating apparent discrepancies between some notions expected to be equivalent. The presented mathematical results are all mechanically checked with the interactive theorem prover Coq, building on existing formalizations of RTA and NC. Establishing such a link between NC and RTA paves the way for improved real-time analyses obtained by combining both theories to enjoy their respective strengths (e.g., multicore analyses for RTA or clock drifts for NC).

DOI

DOI : 10.4230/DARTS.8.1.3

Accès au texte intégral et bibtex

titre

How realistic are claims about the benefits of using digital technologies for GHG emissions mitigation?

auteur

Aina Rasoldier, Jacques Combaz, Alain Girault, Kevin Marquet, Sophie Quinton

resume

While the direct environmental impacts of digital technologies are now well documented, it is often said that they could also help reduce greenhouse gas (GHG) emissions significantly in many domains such as transportation, building, manufacturing, agriculture, and energy. Assessing such claims is essential to avoid delaying alternative action or research. This also applies to related claims about how much GHG emissions existing digital technologies are already avoiding. In this paper, we point out critical issues related to these topics in the state of the art. First, most papers do not provide enough details on the scenarios underlying their evaluations: which hypotheses they are based on and why, and why specific scenarios are chosen as the baseline. This is a key point because it may lead to overestimating the current or potential benefits of digital solutions. Second, results are rarely discussed in the context of global strategies for GHG emissions reduction. These leaves open how the proposed technologies would fit into a realistic plan for meeting current GHG reduction goals. To overcome the underlined limitations, we propose a set of guidelines that all studies on digital solutions for mitigating GHG emissions should satisfy, point out overlooked research directions, and provide concrete examples and initial results for the specific case of carpooling.

Accès au texte intégral et bibtex

2021

Journal articles

titre

System-level Logical Execution Time: Augmenting the Logical Execution Time Paradigm for Distributed Real-Time Automotive Software

auteur

Kai-Björn Gemlau, Leonie Köhler, Rolf Ernst, Sophie Quinton

DOI

DOI : 10.1145/3381847

Accès au texte intégral et bibtex

Reports

titre

CertiCAN: Certifying CAN Analyses and Their Results

auteur

Pascal Fradet, Xiaojie Guo, Sophie Quinton

resume

We present CertiCAN, a tool produced using the Coq proof assistant for the formal certification of CAN analysis results. Result certification is a process that is lightweight and flexible compared to tool certification. Indeed, the certification of an industrial analyzer needs access to the source code, requires the proof of many optimizations or implementation tricks and new proof effort at each software update. In contrast, CertiCAN only relies on the result provided by such a tool and remains independent of the tool itself or its updates. Furthermore, it is usually more time efficient to check a result than to produce it. All these reasons make CertiCAN a practical choice for industrial purposes. CertiCAN is based on the certification and combined use of two well-known CAN analysis tech- niques completed with additional optimizations. Experiments demonstrate that CertiCAN is com- putationally efficient and faster than the underlying combined analysis. It is able to certify the results of RTaW-Pegase, an industrial CAN analysis tool, even for large systems. This result paves the way for a broader acceptance of formal tools for the certification of real-time systems analysis results.

Accès au texte intégral et bibtex

2020

Journal articles

titre

Weakly-hard Real-time Guarantees for Earliest Deadline First Scheduling of Independent Tasks

auteur

Zain a H Hammadeh, Sophie Quinton, Rolf Ernst

resume

The current trend in modeling and analyzing real-time systems is toward tighter yet safe timing constraints. Many practical real-time systems can de facto sustain a bounded number of deadline-misses, i.e., they have Weakly-Hard Real-Time (WHRT) constraints rather than hard real-time constraints. Therefore, we strive to provide tight Deadline Miss Models (DMMs) in complement to tight response time bounds for such systems. In this work, we bound the distribution of deadline-misses for task sets running on uniprocessors using the Earliest Deadline First (EDF) scheduling policy. We assume tasks miss their deadlines due to transient overload resulting from sporadic jobs, e.g., interrupt service routines. We use Typical Worst-Case Analysis (TWCA) to tackle the problem in this context. Also, we address the sources of pessimism in computing DMMs, and we discuss the limitations of the proposed analysis. This work is motivated by and validated on a realistic case study inspired by industrial practice (satellite on-board software) and on a set of synthetic test cases. The synthetic experiment is dedicated to extensively study the impact of EDF on DMMs by presenting a comparison between DMMs computed under EDF and Rate Monotonic (RM). The results show the usefulness of this approach for temporarily overloaded systems when EDF scheduling is considered. They also show that EDF is especially well for WHRT tasks.

DOI

DOI : 10.1145/3356865

Accès au texte intégral et bibtex

2019

Reports

titre

Sciences, Environnements et Sociétés

auteur

Françoise Berthoud, Pascal Guitton, Laurent Lefèvre, Sophie Quinton, Antoine Rousseau, Jacques Sainte-Marie, Céline Serrano, Jean-Bernard Stefani, Peter Sturm, Eric Tannier

resume

Ce document est le résultat du travail du Groupe de Travail (GT) MakeSEnS, chargé par la direction d’Inria de faire des propositions pour que l’institut se saisisse des enjeux environnementaux actuels. Il propose une liste d’actions concrètes à mettre en place pour aider tant les directions nationales que l’ensemble des membres d’Inria à s’informer et à agir à tous les niveaux : individuel, équipes, services, centres, comités et commissions ainsi qu’à l’échelle de l’institut.

Accès au texte intégral et bibtex

2018

Journal articles

titre

Improving and Estimating the Precision of Bounds on the Worst-Case Latency of Task Chains

auteur

Alain Girault, Christophe Prévot, Sophie Quinton, Rafik Henia, Nicolas Sordon

resume

One major issue that hinders the use of performance analysis in industrial design processes is the pessimism inherent to any analysis technique that applies to realistic system models. Indeed, such analyses may conservatively declare unschedulable systems that will in fact never miss any deadlines. We advocate the need to compute not only tight upper bounds on worst-case behaviors, but also tight lower bounds. As a first step, we focus on uniprocessor systems executing a set of sporadic or periodic hard real-time task chains. Each task has its own priority, and the chains are scheduled according to the fixed-priority preemptive scheduling policy. Computing the worst-case end-to-end latency (WCEL) of each chain is complex because of the intricate relationship between the task priorities. Compared to the state of the art, our analysis provides upper bounds on the WCEL in the more general case of asynchro-nous task chains, and also provides lower bounds on the WCEL both for synchronous and asynchronous chains. Our computed lower bounds correspond to actual system executions exhibiting a behavior that is as close to the worst case as possible, while all other approaches rely on simulations. Extensive experiments show the relevance of lower bounds on the worst-case behavior for the industrial design of real-time embedded systems. CCS CONCEPTS • Computer systems organization → Embedded systems; KEYWORDS Worst-case end to end latency, Latency analysis, Task chains ACM Reference format:

DOI

DOI : 10.1109/TCAD.2018.2861016

Accès au texte intégral et bibtex

titre

The Logical Execution Time Paradigm: New Perspectives for Multicore Systems (Dagstuhl Seminar 18092)

auteur

Rolf Ernst, Stefan Kuntz, Sophie Quinton, Martin Simons

resume

This report documents the program and the outcomes of Dagstuhl Seminar 18092 “The Logical Execution Time Paradigm: New Perspectives for Multicore Systems”. The seminar brought together academic and industrial researchers working on challenges related to the Logical Execution Time Paradigm (LET). The main purpose was to promote a closer interaction between the subcommunities involved in the application of LET to multicore systems, with a particular emphasis on the automotive domain.

DOI

DOI : 10.4230/DagRep.8.2.122

Accès au texte intégral et bibtex

Conference papers

titre

A Generic Coq Proof of Typical Worst-Case Analysis

auteur

Pascal Fradet, Maxime Lesourd, Jean-François Monin, Sophie Quinton

resume

This paper presents a generic proof of Typical Worst-Case Analysis (TWCA), an analysis technique for weakly-hard real-time uniprocessor systems. TWCA was originally introduced for systems with fixed priority preemptive (FPP) schedulers and has since been extended to fixed-priority nonpreemptive (FPNP) and earliest-deadline-first (EDF) schedulers. Our generic analysis is based on an abstract model that characterizes the exact properties needed to make TWCA applicable to any system model. Our results are formalized and checked using the Coq proof assistant along with the Prosa schedulability analysis library. Our experience with formalizing real-time systems analyses shows that this is not only a way to increase confidence in our claimed results: The discipline required to obtain machine checked proofs helps understanding the exact assumptions required by a given analysis, its key intermediate steps and how this analysis can be generalized.

Accès au texte intégral et bibtex

titre

A Generalized Digraph Model for Expressing Dependencies

auteur

Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton

resume

In the context of computer assisted verification of schedulability analyses, very expressive task models are useful to factorize the correctness proofs of as many analyses as possible. The digraph task model seems a good candidate due to its powerful expressivity. Alas, its ability to capture dependencies between arrival and execution times of jobs of different tasks is very limited. We propose here a task model that generalizes the digraph model and its corresponding analysis for fixed-priority scheduling with limited preemption. A task may generate several types of jobs, each with its own worst-case execution time, priority, non-preemptable segments and maximum jitter. We present the correctness proof of the analysis in a way amenable to its formalization in the Coq proof assistant. Our objective (still in progress) is to formally certify the analysis for that general model such that the correctness proof of a more specific (standard or novel) analysis boils down to specifying and proving its translation into our model. Furthermore, expressing many different analyses in a common framework paves the way for formal comparisons.

DOI

DOI : 10.1145/3273905.3273918

Accès au texte intégral et bibtex

titre

Building Correct Cyber-Physical Systems: Why we need a Multiview Contract Theory

auteur

Susanne Graf, Sophie Quinton, Alain Girault, Gregor Gössler

resume

The design and verification of critical cyber-physical systems is based on a number of models (and corresponding analysis techniques and tools) representing different viewpoints such as function, timing, security and many more. Overall correctness is guaranteed by mostly informal, and therefore basic, arguments about the relationship between these viewpoint-specific models. We believe that a more flexible contract-based approach could lead to easier integration, to relaxed assumptions, and consequently to more cost efficient systems while preserving the current modelling approach and its tools.

DOI

DOI : 10.1007/978-3-030-00244-2_2

Accès au texte intégral et bibtex

titre

Evaluation and Comparison of Real-Time Systems Analysis Methods and Tools

auteur

Sophie Quinton

resume

The verification of real-time systems has been an active area of research for several decades now. Some results have been successfully transferred to industry. Still, many obstacles remain that hinder a smooth integration of academic research and industrial application. In this extended abstract, we discuss some of these obstacles and ongoing research and community efforts to bridge this gap. In particular, we present several experimental and theoretical methods to evaluate and compare real-time systems analysis methods and tools.

DOI

DOI : 10.1007/978-3-030-00244-2_19

Accès au texte intégral et bibtex

titre

Verifying Weakly-Hard Real-Time Properties of Traffic Streams in Switched Networks

auteur

Leonie Ahrendts, Sophie Quinton, Thomas Boroske, Rolf Ernst

resume

In this paper, we introduce the first verification method which is able to provide weakly-hard real-time guarantees for tasks and task chains in systems with multiple resources under partitioned scheduling with fixed priorities. Existing weakly-hard real-time verification techniques are restricted today to systems with a single resource. A weakly-hard real-time guarantee specifies an upper bound on the maximum number m of deadline misses of a task in a sequence of k consecutive executions. Such a guarantee is useful if a task can experience a bounded number of deadline misses without impacting the system mission. We present our verification method in the context of switched networks with traffic streams between nodes, and demonstrate its practical applicability in an automotive case study.

DOI

DOI : 10.4230/LIPIcs.ECRTS.2018.15

Accès au texte intégral et bibtex

Reports

titre

System Level LET with Application to Automotive Design

auteur

Rolf Ernst, Leonie Ahrendts, Kai-Björn Gemlau, Sophie Quinton, Hermann von Hasseln, Julien Hennig

resume

The logical execution time (LET) programming model has been applied in the automotive industry to master multicore programming of large task systems with complex dependencies. Recent developments in electric powertrains and autonomous vehicle functions raise parallel programming from the multicore level to the vehicle level where the requirements for LET application do not hold any more. This paper introduces System Level LET (SL LET), an extension of LET with relaxed synchronization requirements. While related extensions have been proposed for specific scheduling and communication models before, SL LET can be used with a variety of scheduling algorithms and communication semantics. Furthermore, it can be applied to systems with combinations of LET and other programming models. Yet, SL LET allows end-to-end timing guarantees and preserves essential LET properties required for automotive systems. For illustration, we apply the model to an electric vehicle use case.

Accès au texte intégral et bibtex

2017

Journal articles

titre

Exploiting Execution Dynamics in Timing Analysis Using Job Sequences

auteur

Leonie Ahrendts, Sophie Quinton, Rolf Ernst

resume

Worst case design as needed for critical systems usually resorts to established methods for worst case response time analysis which rely on the worst case execution time of tasks and the minimum temporal distance between task activations. The result is often very pessimistic when compared to the real worst case load. Many feasible designs are therefore rejected under such analyses. Using worst case models based on job sequences rather than single jobs leads to less pessimistic results and makes worst case design more practical. This paper outlines existing modeling and analysis techniques which are based on job sequences and refers to several examples from automotive design where great benefits were demonstrated.

DOI

DOI : 10.1109/MDAT.2017.2746638

Accès au texte intégral et bibtex

Conference papers

titre

Work In Progress: Toward a Coq-certified Tool for the Schedulability Analysis of Tasks with Offsets

auteur

Xiaojie Guo, Sophie Quinton, Pascal Fradet, Jean-François Monin

resume

This paper presents the first steps toward a formally proven tool for schedulability analysis of tasks with offsets. We formalize and verify the seminal response time analysis of Tindell by extending the Prosa proof library, which is based on the Coq proof assistant. Thanks to Coq’s extraction capabilities, this will allow us to easily obtain a certified analyzer. Additionally, we want to build a Coq certifier that can verify the correctness of results obtained using related (but uncertified), already existing analyzers. Our objective is to investigate the advantages and drawbacks of both approaches, namely the certified analysis and the certifier. The work described in this paper as well as its continuation is intended to enrich the Prosa library.

Accès au texte intégral et bibtex

titre

Finite Ready Queues As a Mean for Overload Reduction in Weakly-Hard Real-Time Systems

auteur

Sophie Quinton, Leonie Ahrendts, Rolf Ernst

resume

Finite ready queues, implemented by buuers, are a system reality in embedded real-time computing systems and networks. The dimen-sioning of queues is subject to constraints in industrial practice, and often the queue capacity is suucient for typical system behavior but is not suucient in peak overload conditions. This may lead to overrow and consequently to the discarding of jobs. In this paper, we explore whether nite queue capacity can also be used as a mean of design in order to reduce workload peaks and thus shorten a transient overload phase. We present an analysis method which is to the best of our knowledge the rst one able to give (a) worst-case response times guarantees as well as (b) weakly-hard guarantees for tasks which are executed on a computing system with nite queues. Experimental results show that nite queue capacity may only a have weak overload limiting eeect. This unexpected outcome can be explained by the system behavior in the worst-case corner cases. The analysis shows nevertheless that a trade-oo between weakly-hard guarantees and queue sizes is possible.

DOI

DOI : 10.1145/3139258.3139259

Accès au texte intégral et bibtex

titre

A Framework for Evaluating Schedulability Analysis Tools

auteur

Lijun Shan, Susanne Graf, Sophie Quinton, Loïc Fejoz

resume

There exists a large variety of schedulability analysis tools based on dierent, often incomparable timing models. This variety makes it dicult to choose the best t for analyzing a given real-time system. To help the research community to better evaluate analysis tools and their underlying methods, we are developing a framework which consists of (1) a simple language called RTSpec for specifying real-time systems, (2) a tool chain which translates a system specication in RTSpec into an input for various analysis tools, and (3) a set of benchmarks. Our goal is to enable users and developers of schedulability analysis tools to compare such tools systematically, automatically and rigorously.

Accès au texte intégral et bibtex

titre

Budgeting Under-Specified Tasks for Weakly-Hard Real-Time Systems

auteur

Zain a H Hammadeh, Sophie Quinton, Marco Panunzio, Rafik Henia, Laurent Rioux, Rolf Ernst

resume

In this paper, we present an extension of slack analysis for budgeting in the design of weakly-hard real-time systems. During design, it often happens that some parts of a task set are fully specified while other parameters, e.g. regarding recovery or monitoring tasks, will be available only much later. In such cases, slack analysis can help anticipate how these missing parameters can influence the behavior of the whole system so that a resource budget can be allocated to them. It is, however, sufficient in many application contexts to budget these tasks in order to preserve weakly-hard rather than hard guarantees. We thus present an extension of slack analysis for deriving task budgets for systems with hard and weakly-hard requirements. This work is motivated by and validated on a realistic case study inspired by industrial practice. 1998 ACM Subject Classification B.8.2 Performance Analysis and Design Aids

DOI

DOI : 10.4230/LIPIcs.ECRTS.2017.17

Accès au texte intégral et bibtex

titre

Bounding Deadline Misses in Weakly-Hard Real-Time Systems with Task Dependencies

auteur

Zain A. H. Hammadeh, Rolf Ernst, Sophie Quinton, Rafik Henia, Laurent Rioux

resume

Real-time systems with functional dependencies between tasks often require end-to-end (as opposed to task-level) guarantees. For many of these systems, it is even possible to accept the possibility of longer end-to-end delays if one can bound their frequency. Such systems are called weakly-hard. In this paper we provide end-to-end deadline miss models for systems with task chains using Typical Worst-Case Analysis (TWCA). This bounds the number of potential deadline misses in a given sequence of activations of a task chain. To achieve this we exploit task chain properties which arise from the priority assignment of tasks in static-priority preemptive systems. This work is motivated by and validated on a realistic case study inspired by industrial practice and derived synthetic test cases.

Accès au texte intégral et bibtex

Poster communications

titre

Demo Abstract: Bounding Deadline Misses for Weakly-Hard Real-Time Systems Designed in CAPELLA

auteur

Rafik Henia, Laurent Rioux, Nicolas Sordon, Zain a H Hammadeh, Rolf Ernst, Sophie Quinton

resume

Real-time systems with functional dependencies between tasks often require guarantees on end-to-end delays. For many of these systems, end-to-end deadline misses are accepted if one can limit their frequency. Such systems are called weakly-hard. Recent work has shown that typical worst-case analysis (TWCA) can compute an upper bound on the number of potential deadline misses in a sequence of activations of a task chain. In a joint collaboration between Thales and TU Braunschweig, the use of TWCA to limit the number of deadline misses in an aerial video tracking (AVT) system was evaluated. The AVT case-study, the complete automated model-based tool chain from the design environment to the timing verification using TWCA, as well as the results of the evaluation will be presented in the demonstration. The tool chain involves four tools: the design modeling tool CAPELLA extended by a performance viewpoint which allows annotating the design model with timing properties needed to perform TWCA, the pivot model TEMPO which handles mismatches between the semantics of the design model and the semantics of the model used in TWCA, the scheduling analysis tool pyCPA that performs TWCA and finally the graphical tool TimingGraphics used to visualize the TWCA results. To show the pertinence of the use of TWCA, we will also compare in the demonstration the obtained results with those obtained using worst-case analysis and simulation.

Accès au texte intégral et bibtex

2016

Conference papers

titre

Quantifying the Flexibility of Real-Time Systems

auteur

Rafik Henia, Alain Girault, Christophe Prévot, Sophie Quinton, Laurent Rioux

resume

In this paper we define the flexibility of a system as its capability to schedule a new task. We present an approach to quantify the flexibility of a system. More importantly, we show that it is possible under certain conditions to identify the task that will directly induce the limitations on a possible software update. If performed at design time, such a result can be used to adjust the system design by giving more slack to the limiting task. We illustrate how these results apply to a simple system.

Accès au texte intégral et bibtex

titre

Using Multi-Viewpoint Contracts for Negotiation of Embedded Software Updates

auteur

Sönke Holthusen, Sophie Quinton, Ina Schaefer, Johannes Schlatow, Martin Wegner

resume

In this paper we address the issue of change after deployment in safety-critical embedded system applications. Our goal is to substitute lab-based verification with in-field formal analysis to determine whether an update may be safely applied. This is challenging because it requires an automated process able to handle multiple viewpoints such as functional correctness, timing, etc. For this purpose, we propose an original methodology for contract-based negotiation of software updates. The use of contracts allows us to cleanly split the verification effort between the lab and the field. In addition, we show how to rely on existing viewpoint-specific methods for update negotiation. We illustrate our approach on a concrete example inspired by the automotive domain.

DOI

DOI : 10.4204/EPTCS.208.3

Accès au texte intégral et bibtex

Proceedings

titre

Work-in-Progress and Demo Proceedings – 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)

auteur

Vincent Nélis, Sophie Quinton

resume

This document is a collection of the Work-in-Progress and Demo papers presented at the 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS).

Accès au texte intégral et bibtex

Reports

titre

RTLib: A Library of Timed Automata for Modeling Real-Time Systems

auteur

Lijun Shan, Susanne Graf, Sophie Quinton

resume

There exists a large variety of schedulability analysis tools based on different, often incomparable timing analysis models. This variety makes it difficult to choose the best fit for analyzing a given real-time system. We have developed RTLib, a library of timed automata templates that represent the semantics of a large variety of timing related concepts proposed by existing models and corresponding timing analysis tools. The key specificity of RTLib is that it is structured to be modular, such that (1) defining a new variant of a given concept requires only a localized change, and (2) non contradictory variants can be trivially combined. The extensibility of RTLib is demonstrated using five examples ranging from simple variants of the task activation model to the more complex mixed-criticality paradigm. RTLib provides the formal basis needed to compare the concepts offered by models of different timing analysis tools at the semantic level. This in turn will allow us to provide a syntactic mapping between the input of different tools. Our final goal is to help the research community to better evaluate analysis models and their underlying methods.

Accès au texte intégral et bibtex

2015

Journal articles

titre

Knowledge-based construction of distributed constrained systems

auteur

Susanne Graf, Sophie Quinton

resume

The problem of deriving distributed implementations from global specifications has been extensively studied for a number of application domains. We explore it here from the knowledge perspective: A process may decide to take a local action when it has enough knowledge to do so. Such knowledge may be acquired by communication through primitives available on the platform or by static analysis. In this paper, we want to combine control and distribution, that is, we need to impose some global control constraint on a system executed in a distributed fashion. To reach that goal, we compare two approaches: either build a centralized controlled system, distribute its controller and then implement this controlled system on a distributed platform; or alternatively, directly enforce the control constraint while implementing the distributed system on the platform. We show how to achieve a solution following the second approach and explain why this is a pragmatic and more efficient strategy than the other, previously proposed one.

DOI

DOI : 10.1007/s10270-014-0451-z

Accès au bibtex

Conference papers

titre

Mixed criticality systems with weakly-hard constraints

auteur

Oliver Gettings, Sophie Quinton, Robert Davis

resume

Current adaptive mixed criticality scheduling policies assume a high criticality mode in which all low criticality tasks are descheduled to ensure that high criticality tasks can meet timing constraints derived from certification approved methods. In this paper we present a new scheduling policy, Adaptive Mixed Criticality – Weakly Hard, which provides a guaranteed minimum quality of service for low criticality tasks in the event of a criticality mode change. We derive response time based schedulability tests for this model. Empirical evaluations are then used to assess the relative performance against previously published policies and their schedulability tests.

DOI

DOI : 10.1145/2834848.2834850

Accès au bibtex

titre

Improved Deadline Miss Models for Real-Time Systems Using Typical Worst-Case Analysis

auteur

Xu Wenbo, Zain A. H. Hammadeh, Kröller Alexander, Sophie Quinton, Rolf Ernst

resume

We focus on the problem of computing tight deadline miss models for real-time systems, which bound the number of potential deadline misses in a given sequence of activations of a task. In practical applications, such guarantees are often sufficient because many systems are in fact not hard real-time. Our major contribution is a general formulation of that problem in the context of systems where some tasks occasionally experience sporadic overload. Based on this new formulation, we present an algorithm that can take into account fine-grained effects of overload at the input of different tasks when computing deadline miss bounds. Finally, we show in experiments with synthetic as well as industrial data that our algorithm produces bounds that are much tighter than in previous work, in sufficiently short time.

DOI

DOI : 10.1109/ECRTS.2015.29

Accès au bibtex

2014

Conference papers

titre

Formal Analysis of Timing Effects on Closed-loop Properties of Control Software

auteur

Goran Frehse, Arne Hamann, Sophie Quinton, Matthias Wöhrle

resume

The theories underlying control engineering and real-time systems engineering use idealized models that mutually abstract from central aspects of the other discipline. Control theory usually assumes jitter-free sampling and negligible (constant) input-output latencies, disregarding complex real-world timing effects. Real-time systems theory uses abstract performance models that neglect the functional behavior and derives worst-case situations with limited expressiveness for control functions, e.g., in physically dominated automotive systems. In this paper, we propose an approach that integrates state-of-the art timing models into functional analysis. We combine physical, control and timing models by representing them as a network of hybrid automata. Closed-loop properties can then be verified on this hybrid automata network by using standard model checkers for hybrid systems. Since the computational complexity is critical for model checking, we discuss abstract models of timing behavior that seem particularly suited for this type of analysis. The approach facilitates systematic co-engineering between both control and real-time disciplines, increasing design efficiency and confidence in the system. The approach is illustrated by analyzing an industrial example, the control software of an electro-mechanical braking system, with the hybrid model checker SpaceEx.

Accès au bibtex

titre

Extending typical worst-case analysis using response-time dependencies to bound deadline misses

auteur

Zain A. H. Hammadeh, Sophie Quinton, Rolf Ernst

resume

Weakly-hard time constraints have been proposed for applications where occasional deadline misses are permitted. Recently, a new approach called Typical Worst-Case Analysis (TWCA) has been introduced which exploits similar constraints to bound response times of systems with sporadic overload. In this paper, we extend that approach for static priority preemptive and non-preemptive scheduling to determine the maximum number of deadline misses for a given deadline. The approach is based on an optimization problem which trades off higher priority interference versus miss count. We formally derive a lattice structure for the possible combinations that lays the ground for an integer linear programming (ILP) formulation. The ILP solution is evaluated showing effectiveness of the approach and far better results than previous TWCA.

DOI

DOI : 10.1145/2656045.2656059

Accès au bibtex

titre

Typical Worst Case Response-Time Analysis and its Use in Automotive Network Design

auteur

Sophie Quinton, Julien Hennig, Torsten Bone, Moritz Neukirchner, Rolf Ernst, Mircea Negrean

resume

For some automotive applications, worst case performance guarantees are too expensive, but a minimum level of performance must be formally guaranteed. For such applications, we have developed an approach called Typical Worst Case Analysis (TWCA) which can formally bound the number of violations of the computed response-time guarantee in a given time window. In this paper, we demonstrate how it can be used to analyze a real CAN bus with complex load patterns. We investigate the effects of these load patterns and show how the necessary parameters can be derived and verified from traces and specifications. We compare the results to the commonly used base load approximation — like a 50%-limit for cyclic load — showing superior accuracy and expressiveness.

DOI

DOI : 10.1145/2593069.2602977

Accès au bibtex