License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.8.1.3
URN: urn:nbn:de:0030-drops-164990
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16499/
Go back to Dagstuhl Artifacts Series

Roux, Pierre ; Quinton, Sophie ; Boyer, Marc

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

pdf-format:
DARTS-8-1-3.pdf (0.4 MB)

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.

BibTeX - Entry

@Article{roux_et_al:DARTS.8.1.3,
  author =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  title =	{{A Formal Link Between Response Time Analysis and Network Calculus (Artifact)}},
  pages =	{3:1--3:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{1},
  editor =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16499},
  URN =		{urn:nbn:de:0030-drops-164990},
  doi =		{10.4230/DARTS.8.1.3},
  annote =	{Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq}
}

Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq
Collection: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)
Related Scholarly Article: https://doi.org/10.4230/LIPIcs.ECRTS.2022.5
Issue Date: 2022
Date of publication: 28.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI