Every response-time analysis takes a blocking term as input: how long a task can be held up by a lower-priority task holding a resource it needs. In most timing arguments that number is a guess, and it is the weakest number in the argument.
Under a priority-ceiling protocol the bound is derivable from the resource graph. Nobody derives it, because deriving it requires knowing which tasks share which resources — and that information usually exists only in somebody's head.
Nothing is implemented. The design question that has to be settled first is what a resource graph must state to be checkable, and whether that can be extracted from source rather than declared by hand.
A declared graph that disagrees with the code produces a bound about a system nobody is running.
dy-wcet is the piece that works
today: response-time analysis for fixed-priority task sets, in integer
arithmetic that refuses rather than rounds.
Apache-2.0 OR MIT, at your option.