Analyzing Tabular and State-Transition Requirements Specifications in PVS

Sam Owre, John Rushby, and Natarajan Shankar

CSL Technical Report CSL-95-12

Note: this revised edition of the report differs significantly from the draft issued in June 1995.

A shorter version was published in TACAS 97.

Abstract

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 represent 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 manner. We show how PVS can check these tables for well-formedness, and how PVS's model checking capabilities can be used to verify invariants and reachability properties of SCR requirements specifications, and inclusion relations between the behaviors of different specifications.

These examples demonstrate how several capabilities of the PVS language and verification system can be used in combination to provide customized support for specific methodologies for documenting and analyzing requirements. Because they use only the standard capabilities of PVS, users can adapt and extend these customizations to suit their own needs. Those developing dedicated tools for individual methodologies may find these constructions in PVS helpful for prototyping purposes, or as a useful adjunct to a dedicated tool when the capabilities of a full theorem prover are required.

The examples also illustrate the power and utility of an integrated general-purpose system such as PVS. For example, there was no need to adapt or extend the PVS model checker in order to make it work with SCR specifications described using the PVS TABLE construct: the model checker is applicable to any transition relation, independently of the PVS language constructs used in its definition.

dvi
postscript
PVS specification files

BibTeX Entry

@techreport{Owre95:tables,
	TITLE = {Analyzing Tabular and State-Transition Specifications
		in {PVS}},
	AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar},
	NUMBER = {SRI-CSL-95-12},
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	MONTH = jul,
	YEAR = 1995,
	NOTE = {Revised May 1996.
                Available, with specification files, from 
                \url{http://www.csl.sri.com/csl-95-12.html}}
}

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page