A Formal Link Between Response Time Analysis and Network Calculus (Artifact)

Authors Pierre Roux , Sophie Quinton , Marc Boyer



PDF
Thumbnail PDF

Artifact Description

DARTS.8.1.3.pdf
  • Filesize: 413 kB
  • 3 pages

Document Identifiers

Author Details

Pierre Roux
  • ONERA, Toulouse, France
  • DTIS - Université de Toulouse, F-31055 Toulouse, France
Sophie Quinton
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, F-38000 Grenoble, France
Marc Boyer
  • ONERA, Toulouse, France
  • DTIS - Université de Toulouse, F-31055 Toulouse, France

Cite AsGet BibTex

Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus (Artifact). In Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 1, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/DARTS.8.1.3

Artifact

Abstract

Classical Response Time Analysis (RTA) and Network Calculus (NC) are two major formalisms used for the verification of real-time properties. The related paper offer mathematical links between these two different theories. Based on these links, it then proves 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). This artifact enables to reproduce these proofs.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time system specification
  • Networks → Formal specifications
  • Software and its engineering → Formal methods
  • General and reference → Verification
Keywords
  • Response Time Analysis
  • Network Calculus
  • dense time
  • discrete time
  • response time
  • formal proof
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail