Publications of Sophie Quinton

Back to the home page of Sophie Quinton

You can find my publications since 2014 below. Most of my older publications are listed on dblp.

Please note that the paper “Philip Axer, Sophie Quinton, Moritz Neukirchner, Rolf Ernst, Björn Döbel, Hermann Härtig: Response-Time Analysis of Parallel Fork-Join Workloads with Real-Time Constraints” at ECRTS 2013 has a flaw. More information about this is available in Philip Axer’s PhD thesis. Feel free to drop me a line for more information.

Publications HAL de Sophie, Quinton

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
https://hal.inria.fr/hal-01674751/file/DesignAndTest17.pdf 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
https://hal.inria.fr/hal-01629288/file/offset_WiP.pdf 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
https://hal.inria.fr/hal-01674737/file/rtns17.pdf 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
https://hal.inria.fr/hal-01674731/file/KimFest17.pdf BibTex
titre
Budgeting Under-Specified Tasks for Weakly-Hard Real-Time Systems
auteur
Zain 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
https://hal.inria.fr/hal-01674742/file/ECRTS17.pdf 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
https://hal.inria.fr/hal-01426632/file/2017-DATE.pdf 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 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
https://hal.inria.fr/hal-01674754/file/RTAS17.pdf 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
https://hal.inria.fr/hal-01426658/file/JRWRTC_2016_paper_6.pdf 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
https://hal.inria.fr/hal-01426654/file/2016-PrePost.pdf BibTex

Directions of work or 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
https://hal.inria.fr/hal-01305183/file/RTAS-WiP-and-Demo-proceedings.pdf 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
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
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
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
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
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
BibTex

Comments are closed