Publications of Sophie Quinton

Back to the home page of Sophie Quinton

Publications HAL de Sophie, Quinton

2017

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

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