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.