While there has been a large amount of work on validation

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

refine the model and formalize the analysis of a functional timing operator (Held for)

in the PVS theorem prover. We formalize different implementation

environments incorporating nonuniform samples with bounded jitter and

for one of the environments provide a full formal proof of necessary and

sufficient conditions for when it is possible to implement a Held for requirement.

We briefly describe how these results can then be used to

formally verify a sample module implementing a requirement that utilizes

the Held for operator and describe an example application.