Skip to main content
eScholarship
Open Access Publications from the University of California

The use of sequencing information in software specification for verification

Abstract

Software requirements specifications, virtual machine definitions, and algorithmic design all place constraints on the sequence of operations that are permissible during a program's execution. This paper discusses how these constraints can be captured and used to aid in the program verification process. The sequencing constraints can be expressed as a grammar over the alphabet of program operations. Several techniques can be used in support of testing or verification based on these specifications. Dynamic aalysis and static analysis are considered here. The automatic generation of some of these aids is feasible; the means of doing so is described.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View