The authors characterize this paper as a work in progress in computer assisted verification (CAV) of task-scheduling models. Directed graph (digraph) models are expressive; however, as the authors point out, they are limited with respect to “dependencies between arrival and execution times of jobs [components of tasks] of different tasks.” The authors propose their generalized fixed-task-priority with limited preemption task scheduling model GD, which they analyze and verify in some detail in section 6. A coequal goal of this paper is a correctness proof of response time analysis (RTA) that is formalizable in the syntax and semantics of the Coq [1,2] proof assistant as an enhancement of Prosa, a Coq library of schedulability results that comprises formal specifications and Coq (mechanized) proofs of schedulability analysis.
Section 2 employs a concrete job-level fixed-priority limited preemptive (JFPLP) scheduler to explicate system behavior, including priority, arrival time, jitter, and execution time costs. Service time is to be formalized in Coq. Figure 2 in section 3, on the GD model, is a very clear illustration of job types as (graph) vertices, edges labeled with inter-arrival times of jobs of different types, and cost vectors of non-preemptable job segments. The notation of the text is necessarily quite intricate, needing more than casual attention. Section 4 reports that GD expresses a variety of existing task models, and generalizes the digraph real-time task (DRT) model [3].
Sections 5 and 6 are statements and (non-Coq) correctness proofs of RTAs. The heart of the paper, these substantiate RTA correctness via classical (my term), that is, non-machine-generated proofs.
This work will certainly inform those already immersed in RTA of the current state and direction of the art, with the Coq formalization a substantial bonus. Students and neophytes can profit by reading [3] first.
