There are many ways in which one could possibly employ a proof assistant to formalize real-time scheduling. Not all such approaches are equally fruitful. Prosa is an opinionated framework that is aimed at an audience without much prior experience with formal proofs, guided by the following goals and principles.
To ensure that the Prosa framework is useful and yet feasible in the long term, we established three basic goals.
Prosa is an open-source project to enable peer review and community involvement. As a long-term goal, we envision a shared repository of formal definitions and proofs for most major results in real-time scheduling.
As Prosa’s shared specification of common concepts such as “sporadic tasks”, “constrained deadlines”, “identical multiprocessors”, etc., is reviewed and becomes widely accepted, mechanized proofs built on this foundation provide an opportunity for trustworthy, non-disputable results. By increasing the level of confidence in schedulability analysis, it is our hope that a formal foundation will eventually help in convincing practitioners to more readily adopt modern real-time resource management approaches, especially in the context of safety-critical systems subject to certification requirements.
Given that the literature on real-time scheduling is vast, we focus our finite resources on those aspects of scheduling theory that are most relevant from a safety perspective. In particular, in schedulability proofs, we prioritize sufficient over necessary conditions and other secondary issues, such as algorithm termination or time complexity.
When deploying safety-critical systems, the scenario that must be prevented at all costs is the use of potentially unsound analysis. In contrast, the failure modes of other possible issues such as a fixed-point search that fails to converge, accidental pessimism, or an erroneously derived time or memory complexity bound are either readily apparent to the engineer (e.g., the analysis times out or unexpectedly claims a system to be unschedulable) or are of interest only to the academic community.
Nevertheless, Prosa is expressive enough to define and prove some of these additional properties.
Prosa specifically targets researchers in the development of provably-correct schedulability analyses. Real-time systems engineers and other practitioners will instead indirectly benefit from the artifacts of this research. In particular, tool providers can implement analyses that are guaranteed to be correct, and can also test their implementations against provably correct reference models in Prosa. As a result, end users will eventually benefit from better tools and safer systems.
To become and remain as accessible as possible, Prosa sticks to the following principles.
The correctness of a mechanized proof only goes as far as the correctness of the underlying specification, which must still be manually vetted and accepted as valid by the community at large. Hence, formal definitions and theorem statements should be as easily understood as their pen-and-paper counterparts.
Our primary goal is to make the specification accessible to researchers familiar with real-time scheduling who do not necessarily have a background in formal methods. As part of our coding style, we favor the following guidelines.
Many lemmas, short proofs: To make proof strategies easy to follow, we split the proof of theorems into many short lemmas (so that each proof script spans at most a few dozen lines of code). This makes it possible to understand the proof outline at a high level without diving into low-level proof scripts.
Long, verbose names: Our definitions and lemmas have verbose names to make statements self-contained and clear, so that the flow of the proof can be easily followed even without understanding each formal definition in detail.
Heavy use of documentation: We exploit Coq documentation facilities (e.g., coqdoc) to make the experience of reading a specification closer to that of reading a paper. In particular, we intersperse paper-like explanations and matching formal statements to provide guidance to the reader.
See also the Prosa writing and coding guidelines.
Excessive generality and abstraction can harm readability, as it creates clutter, indirection, and numerous dependencies across many files and definitions. In contrast to traditional software engineering guidelines, we favor redundancy and immediacy over reuse and abstraction in our definitions.
By doing so, we intentionally favor novice readers (who can focus on the subject matter, i.e., scheduling and questions of timeliness) over experienced authors of specifications and proofs (who are forced to produce more code). This is a deliberate choice in line with the observation that formal proofs are of limited value if they are ignored by the community at large — to be successful, a formal specification must be read much more often than it is written.
Instead of radically changing the way that proofs are carried out (e.g., by switching to temporal logics that are expressive, yet cryptic to the uninitiated), we believe that a universal formal specification of real-time scheduling should reuse the common notation and proof style familiar to real-time scheduling experts. Doing so not only allows existing results to be more easily formalized, but also makes our formalization of scheduling concepts more accessible to readers with a background in real-time scheduling.
In our specification, we try not to use any complex logics or Coq features that go beyond common mathematical concepts (e.g., we avoid records, canonical structures, etc.), other than in a few exceptional cases for simplicity or compatibility with libraries. Rather, we favor first-order logic, lists, functions and Peano arithmetic; basic concepts that are readily familiar to any computer scientist.
(That said, the full power of Coq remains available for any concepts and proofs that do not easily fit into these confines.)