Abstract:
There has been relatively little work on the implementability of timing requirements. We have previously provided definitions of funda- mental timing operators that explicitly considered tolerances on property durations and intersample jitter. In this work we identify three environ- mental 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 that implements the Held For operator and then verify it in PVS. This pre-verified component is then used to guide the design of more complex components and to decompose their design verification into simple inductive proofs as demonstrated through the implementation of a timing requirement for an example application.
@inproceedings{HuLawfordWassyng2008,
author = {Xiayong Hu and Mark Lawford and Alan Wassyng},
title = {Formal Verification of the Implementability of Timing Requirements},
editor = {D. Cofer and A. Fantechi},
booktitle = {Formal Methods in Industry Critical Systems},
series = {{LNCS}},
volume = {5596},
pages = {119--134},
year = {2009},
location = {L'Aquila, Italy},
publisher = {Springer}
}