Formal Verification of the Implementability of Timing Requirements

by X. Hu, M. Lawford and A. Wassyng


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.


 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}

Mark Lawford
Last modified: Sat May 5 14:11:50 IST 2007