Electronic Resource
Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle
| العنوان: | Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle |
|---|---|
| المؤلفون: | Sergey Bozhko and Björn B. Brandenburg, Bozhko, Sergey, Brandenburg, Björn B. |
| بيانات النشر: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik 2020 |
| نوع الوثيقة: | Electronic Resource |
| مستخلص: | 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. |
| مصطلحات الفهرس: | hard real-time systems, response-time analysis, uniprocessor, busy window, fixed priority, EDF, verification, Coq, Prosa, preemptive, non-preemptive, limited-preemptive, InProceedings, Text, doc-type:ResearchArticle, publishedVersion |
| DOI: | 10.4230.LIPIcs.ECRTS.2020.22 |
| URL: | Is Part Of LIPIcs, Volume 165, 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020) |
| الاتاحة: | Open access content. Open access content https://creativecommons.org/licenses/by/3.0/legalcode |
| ملاحظة: | application/pdf English |
| Other Numbers: | DEDAG oai:drops-oai.dagstuhl.de:12385 doi:10.4230/LIPIcs.ECRTS.2020.22 urn:nbn:de:0030-drops-123850 1358727285 |
| المصدر المساهم: | SCHLOSS DAGSTUHL LEIBNIZ ZENTRUM GMBH From OAIster®, provided by the OCLC Cooperative. |
| رقم الانضمام: | edsoai.on1358727285 |
| قاعدة البيانات: | OAIster |
| DOI: | 10.4230.LIPIcs.ECRTS.2020.22 |
|---|