DROPS

Document

Artifact

Foundational Response-Time Analysis as Explainable Evidence of Timeliness (Artifact)

Authors: Marco Maida, Sergey Bozhko, and Björn B. Brandenburg

Published in: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)

Abstract

This artifact provides the means to validate and reproduce the results of the associated paper “Foundational Response-Time Analysis as Explainable Evidence of Timeliness”. The artifact demonstrates how to (i) generate task sets needed to run the experiments, (ii) prepare and run POET on the generated input, (iii) plot the figures presented in the paper, and (iv) visually inspect the generated certificates.

Cite as

Marco Maida, Sergey Bozhko, and Björn B. Brandenburg. Foundational Response-Time Analysis as Explainable Evidence of Timeliness (Artifact). In Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 1, pp. 7:1-7:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{maida_et_al:DARTS.8.1.7,
  author =	{Maida, Marco and Bozhko, Sergey and Brandenburg, Bj\"{o}rn B.},
  title =	{{Foundational Response-Time Analysis as Explainable Evidence of Timeliness (Artifact)}},
  pages =	{7:1--7:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{1},
  editor =	{Maida, Marco and Bozhko, Sergey and Brandenburg, Bj\"{o}rn B.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.1.7},
  URN =		{urn:nbn:de:0030-drops-165038},
  doi =		{10.4230/DARTS.8.1.7},
  annote =	{Keywords: hard real-time systems, response-time analysis, uniprocessor, Coq, Prosa, fixed priority, EDF, preemptive, non-preemptive, verification}
}

Document

DOI: 10.4230/LIPIcs.ECRTS.2022.19

Foundational Response-Time Analysis as Explainable Evidence of Timeliness

Authors: Marco Maida, Sergey Bozhko, and Björn B. Brandenburg

Published in: LIPIcs, Volume 231, 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)

Abstract

The paper introduces foundational response-time analysis (RTA) as a means to produce strong and independently checkable evidence of temporal correctness. In a foundational RTA, each response-time bound calculated comes with an auto-generated certificate of correctness - a short and human-inspectable sequence of machine-checked proofs that formally show the claimed bound to hold. In other words, a foundational RTA yields explainable results that can be independently verified (e.g., by a certification authority) in a rigorous manner (with an automated proof checker). Consequently, the analysis tool itself does not need to be verified nor trusted. As a proof of concept, the paper presents POET, the first foundational RTA tool. POET generates certificates based on Prosa, the to-date largest verified framework for schedulability analysis, which is based on Coq. The trusted computing base is hence reduced to the Coq proof checker and its dependencies. POET currently supports two scheduling policies (earliest-deadline-first, fixed-priority), two preemption models (fully preemptive, fully non-preemptive), arbitrary deadlines, periodic and sporadic tasks, and tasks characterized by arbitrary arrival curves. The paper describes the challenges inherent in the development of a foundational RTA tool, discusses key design choices, and reports on its scalability.

Cite as

Marco Maida, Sergey Bozhko, and Björn B. Brandenburg. Foundational Response-Time Analysis as Explainable Evidence of Timeliness. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 19:1-19:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{maida_et_al:LIPIcs.ECRTS.2022.19,
  author =	{Maida, Marco and Bozhko, Sergey and Brandenburg, Bj\"{o}rn B.},
  title =	{{Foundational Response-Time Analysis as Explainable Evidence of Timeliness}},
  booktitle =	{34th Euromicro Conference on Real-Time Systems (ECRTS 2022)},
  pages =	{19:1--19:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-239-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{231},
  editor =	{Maggio, Martina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2022.19},
  URN =		{urn:nbn:de:0030-drops-163363},
  doi =		{10.4230/LIPIcs.ECRTS.2022.19},
  annote =	{Keywords: hard real-time systems, response-time analysis, uniprocessor, Coq, Prosa, fixed priority, EDF, preemptive, non-preemptive, verification}
}

Search Results

Documents authored by Maida, Marco

Foundational Response-Time Analysis as Explainable Evidence of Timeliness (Artifact)

Abstract

Cite as

Foundational Response-Time Analysis as Explainable Evidence of Timeliness

Abstract

Cite as

Thanks for your feedback!

Could not send message