POET is the first implementation of a foundational response-time analysis. In short, POET produces proof-carrying response-time bounds that can be verified independently of the (unverified) tool that computed them. The generated proofs build extensively on Prosa.
Both the tool itself and the approach in general are discussed in detail in an ECRTS 2022 paper:
Given a YAML-encoded description of a workload comprised of sporadic or periodic real-time tasks to be scheduled on a uniprocessor, POET will (a) first perform a response-time analysis and then generate a Prosa-based certificate of correctness for each task that formally proves the computed response-time bound to be correct. Second, (b) the generated certificates are compiled and checked with the Coq toolchain.
There are two primary benefits to the foundational approach realized by POET:
Trustworthy results based on a small TCB containing only standard tools: Neither the underlying theory nor the implementation of the response-time analysis (i.e., POET itself) must be trusted. Only the Coq toolchain and its dependencies form the TCB.
Explainable results: the generated certificates are designed for readability and can be explored by a human to any desired degree of scrutiny. In contrast to a traditional response-time analysis tool, POET’s output is thus fully transparent.
The main challenge that POET needs to overcome is runtime scalability of the Coq proof checker coqchk when faced with with many tasks, complex arrival patterns, and large-magnitude numerical task parameters since Prosa’s specification relies on ssreflect’s unary number representation to model time. To scale to practical workload sizes, POET relies on refinements obtained with CoqEAL.
Please see the paper for an in-depth explanation of the foundational approach and its advantages and challenges, POET’s use of CoqEAL, and an evaluation of POET’s scalability.
The current implementation of POET can be found here:
Please refer to the provided README for installation instructions.
POET was originally developed by Marco Maida and Sergey Bozhko. It is now being maintained by the Prosa project.
Please contact Björn Brandenburg with any questions or comments.