Formal Verification of the Implementability of Timing Requirements

There has been relatively little work on the implementability of timing requirements. We have previously provided definitions of fundamental timing operators that explicitly considered tolerances on property durations and intersample jitter. In this work we identify three environmental assumptions and compare the implementability of a Held_For operator in each of them, formalizing this analysis in PVS. We show how to design a software component …