DARTS.6.1.3.pdf
- Filesize: 275 kB
- 2 pages
Document
Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)
Volume: DARTS, Volume 6 (ECOOP 2020)
Conference: Euromicro Conference on Real-Time Systems (ECRTS)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-06-30
Artifact Description
Document Identifiers
Cite As Get BibTex
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)
https://doi.org/10.4230/DARTS.6.1.3
Artifact
DARTS-6-1-3-artifact-5f10805963fcb235c83f7a7f0be07a52.tgz
(Filesize: 6.42 MB)
MD5 Sum:
5f10805963fcb235c83f7a7f0be07a52
(Get MD5 Sum)
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.
Subject Classification
ACM Subject Classification
- Computer systems organization → Real-time systems
- Software and its engineering → Scheduling
- Theory of computation → Scheduling algorithms
Keywords
- hard real-time systems
- response-time analysis
- uniprocessor
- busy window
- fixed priority
- EDF
- verification
- Coq
- Prosa
- preemptive
- non-preemptive
- limited-preemptive
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads