Search Results

Documents authored by Bozhko, Sergey

Document
Artifact
DOI: 10.4230/DARTS.8.1.7
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}
}
Document
Artifact
DOI: 10.4230/DARTS.6.1.3
Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle (Artifact)

Authors: Sergey Bozhko and Björn B. Brandenburg

Published in: DARTS, Volume 6, Issue 1, Special Issue of the 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)

Abstract
This artifact provides the means to validate and reproduce the results of the associated paper "Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle". In this artifact we demonstrate how to compile the source code and automatically check the proofs of each theorem. We also provide references to all key results claimed to be proven in the paper (including Abstract RTA and all eight instantiations), so that readers may confirm that no proofs have been omitted.
Cite as

Sergey Bozhko and Björn B. Brandenburg. Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle (Artifact). In Special Issue of the 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 1, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{bozhko_et_al:DARTS.6.1.3,
  author =	{Bozhko, Sergey and Brandenburg, Bj\"{o}rn B.},
  title =	{{Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle (Artifact)}},
  pages =	{3:1--3:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{1},
  editor =	{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.6.1.3},
  URN =		{urn:nbn:de:0030-drops-123930},
  doi =		{10.4230/DARTS.6.1.3},
  annote =	{Keywords: hard real-time systems, response-time analysis, uniprocessor, busy window, fixed priority, EDF, verification, Coq, Prosa, preemptive, non-preemptive, limited-preemptive}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2020.22
Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle

Authors: Sergey Bozhko and Björn B. Brandenburg

Published in: LIPIcs, Volume 165, 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)

Abstract
This paper introduces the first general and rigorous formalization of the classic busy-window principle for uniprocessors. The essence of the principle is identified as a minimal set of generic, high-level hypotheses that allow for a unified and general abstract response-time analysis, which is independent of specific scheduling policies, workload models, and preemption policy details. From this abstract core, the paper shows how to obtain concrete analysis instantiations for specific uniprocessor schedulers via a sequence of refinement steps, and provides formally verified response-time bounds for eight common schedulers and workloads, including the widely used fixed-priority (FP) and earliest-deadline first (EDF) scheduling policies in the context of fully, limited-, and non-preemptive sporadic tasks. All definitions and proofs in this paper have been mechanized and verified with the Coq proof assistant, and in fact form the common core and foundation for verified response-time analyses in the Prosa open-source framework for formally proven schedulability analyses.
Cite as

Sergey Bozhko and Björn B. Brandenburg. Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle. In 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 165, pp. 22:1-22:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bozhko_et_al:LIPIcs.ECRTS.2020.22,
  author =	{Bozhko, Sergey and Brandenburg, Bj\"{o}rn B.},
  title =	{{Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle}},
  booktitle =	{32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)},
  pages =	{22:1--22:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-152-8},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{165},
  editor =	{V\"{o}lp, Marcus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2020.22},
  URN =		{urn:nbn:de:0030-drops-123850},
  doi =		{10.4230/LIPIcs.ECRTS.2020.22},
  annote =	{Keywords: hard real-time systems, response-time analysis, uniprocessor, busy window, fixed priority, EDF, verification, Coq, Prosa, preemptive, non-preemptive, limited-preemptive}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact