Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/DARTS.6.1.3
URN: urn:nbn:de:0030-drops-123930
URL: https://drops.dagstuhl.de/opus/volltexte/2020/12393/
Bozhko, Sergey ; Brandenburg, Björn B.
Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle (Artifact)
| pdf-format: |
|
|
| artifact-format: |
|
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.
BibTeX - Entry
@Article{bozhko_et_al:DARTS:2020:12393,
author = {Sergey Bozhko and Bj{\"o}rn B. Brandenburg},
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},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12393},
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}
}
| Keywords: | hard real-time systems, response-time analysis, uniprocessor, busy window, fixed priority, EDF, verification, Coq, Prosa, preemptive, non-preemptive, limited-preemptive | |
| Seminar: | DARTS, Volume 6, Issue 1, Special Issue of the 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020) | |
| Related Scholarly Article: | https://doi.org/10.4230/LIPIcs.ECRTS.2020.22 | |
| Issue date: | 2020 | |
| Date of publication: | 30.06.2020 |
