What Really is pWCET? A Rigorous Axiomatic Proposal

The concept of a probabilistic worst-case execution time (pWCET) has gradually emerged from the work of many authors over the course of 2–3 decades. Intuitively, pWCET is a simplifying model abstraction that safely over-approximates the ground-truth probabilistic execution time (pET) of a real-time task. In particular, when analyzing the cumulative processor demand of multiple jobs, the pWCET abstraction is intended to allow for the use of techniques from probability theory that require random variables to be independent and identically distributed (IID), even though the underlying ground-truth pET random variables are usually not independent. However, while powerful, the pWCET concept is subtle and difficult to define precisely, and easily misinterpreted. To place the pWCET concept on firm, unambiguous mathematical foundations, this paper proposes the first rigorous, axiomatic definition of pWCET that is suitable for formal proof. In addition, an adequacy property is stated that formally captures the intuitive notion of an “IID upper bound on pET.” The proposed pWCET definition is shown to satisfy this adequacy condition, and thereby is the first notion of pWCET for which the IID guarantee is formally established. All definitions and proofs have been verified with the Coq proof assistant.