License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECRTS.2020.22
URN: urn:nbn:de:0030-drops-123850
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12385/
Go to the corresponding LIPIcs Volume Portal

Bozhko, Sergey ; Brandenburg, Björn B.

Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle

pdf-format:
LIPIcs-ECRTS-2020-22.pdf (1.0 MB)

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.

BibTeX - Entry

@InProceedings{bozhko_et_al:LIPIcs:2020:12385,
  author =	{Sergey Bozhko and Bj{\"o}rn B. Brandenburg},
  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 =	{Marcus V{\"o}lp},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12385},
  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}
}

Keywords: hard real-time systems, response-time analysis, uniprocessor, busy window, fixed priority, EDF, verification, Coq, Prosa, preemptive, non-preemptive, limited-preemptive
Collection: 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)
Issue Date: 2020
Date of publication: 30.06.2020
Supplementary Material: ECRTS 2020 Artifact Evaluation approved artifact available at https://doi.org/10.4230/DARTS.6.1.3. The Coq proof, a browsable specification, and artifact evaluation instructions can be found at https://people.mpi-sws.org/~sbozhko/ECRTS20/AbstractRTA.html.

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