Analyzing Tabular and State-Transition Requirements Specifications in PVS
Sam Owre, John Rushby, Natarajan Shankar · NASA Technical Reports Server (NASA) · 1997
We describe PVS's capabilities for representing tabular specifications of the kind advocated by Parnas and others, and show how PVS's Type Correctness Conditions (TCCs) are used to ensure certain well-formedness properties. We then show how these and other capabilities of PVS can be used to repre-sent the AND/OR tables of Leveson and the Decision Tables of Sherry, and we demonstrate how PVS_s TCCs can expose and help isolate errors in the latter. We extend this approach to represent the mode transition tables of the Software Cost Reduction (SCR) method in an attractive rammer. We show how PVS can check these tables for well-formedness, and how PVS's model checking capalfilities can he used to verify invariants and reaehability properties of SCR requirelnents specifications, and inclusion relations between the behaviors of different specifica-tions. These exalnples demonstrate how sew_ral capabilities of the PVS language and verification system can be used in combination to provide customized support for