This web page provides the Coq proof and supplemental materials for the following paper:

- K. Bedarkar, M. Vardishvili, S. Bozhko, M. Maida, and B. Brandenburg, “From Intuition to Coq: A Case Study in Verified Response-Time Analysis of FIFO Scheduling”,
*Proceedings of the 43rd IEEE Real-Time Systems Symposium (RTSS 2022)*, December 2022.

The interested reader is invited to follow the discussion in Section IV of the paper in parallel with the formal Coq development that is being described. For ease of viewing and inspection, two variants of the discussed Coq development are provided:

A static, hyper-linked rendering of the Coq development —

**start with this one**.

As discussed in the paper, the proof builds on Prosa and its abstract RTA framework. (In fact, it has been integrated into Prosa.) It thus leverages a lot of definitions found in Prosa. This rendering of the Coq development is cross-referenced using hyperlinks, which makes it easy to click through to the underlying definitions.

The Ltac proof scripts are contained in static form, but initially hidden. To see a proof script, click on the string`Proof`

that appears after each fact, lemma, and theorem to display their respective proofs.

Note however that Ltac proof scripts are not primarily intended for human consumption. In particular,*Ltac proof scripts are*. Rather, Ltac proof scripts should be “stepped through” interactively to see how each tactic application changes the proof state (i.e., the sets of established facts, assumptions, and remaining proof obligations). To see an example of this, try out the second HTML rendering discussed next.**not**expected to “make sense” when read in static formAn interactive, steppable rendering of the Coq proof — most suitable for readers with

**prior Coq experience**.

This variant use Alectyron to provide an interactive view of the Coq development that allows stepping through the proof. Its main benefit is that it allows readers to explore the proof state,*i.e.*, the effect of individual Ltac tactic invocations, without having to install and run Coq locally.

**Suggested use**: click on “windowed” in the top bar and move the mouse pointer over proof steps to see the proof state change. If the right-hand pane does not fit the screen, decrease your web browser’s font size until it fits.

A Rust implementation of the proposed response-time analysis may be found in the `response-time-analysis`

crate.

More specifically, the function `fifo::dedicated_uniproc_rta`

implements the proposed analysis.

Our artifact evaluation package provides:

- the full Coq development,
- instructions for compiling and checking the proof,
- the code, tools, and scripts underlying the empirical evaluation presented in Section V of the paper, and
- instructions for reproducing the results shown in the figures.

The package may be downloaded here: rtss22-artifact.tgz (1.7 MiB)

Please refer to the `README`

files enclosed in the package for further details.