Report Number: CSL-TR-89-379
Institution: Stanford University, Computer Systems Laboratory
Title: Two Dimensional Pinpointing: An Application of Formal Specification to Debugging Packages
Author: Luckham, David
Date: April 1989
Abstract: New methods of testing and debugging software utilizing high-level formal specifications are presented. These methods require a new generation of support tools. Such tools must be capable of automatically comparing the runtime behavior of hierarchically structured software with high-level specifications; they must provide information about inconsistencies in terms of abstractions used in specifications. This use of specifications has several advantages over present-day debugging methods: (1) the debugging problem itself is precisely defined by specifications; (2) violations of specifications are detected automatically, thus eliminating the need to search output traces and recognize errors manually; (3) complex tests, such as tests for side-effects on global data, can be made easily; (4) the new methods are independent of any compiler and runtime environment for a programming language; (5) they apply generally to hierarchically structured software --- e.g., packages containing nested units, (6) they also apply to other life-cycle processes such as analysis of prototypes, and the use of prototypes to build formal specifications. In this paper a particular process for locating errors in software packages, called two dimensional pinpointing, is described. Tests consist of sequences of package operations (first dimension). Specifications at the highest (most abstract) level are checked first. If violations occur then new specifications are added if possible, otherwise checking of specifications at the next lower level (second dimension) is activated. Violation of a new specification provides more information about the error which reduces the region of program text under suspicion. All interaction between programmer and toolset is phrased in terms of the concepts used to specify the program. Two dimensional pinpointing is presented using the Anna specification language for Ada programs. Anna and a toolset for comparing behavior of Ada programs with Anna specifications is described. Pinpointing techniques are then illustrated by examples. The examples involve debugging of Ada packages, for which Anna provides a rich set of specification constructs. The Anna toolset supports use of the methodology on the full Ada/Anna languages, and is being engineered to commercial standards.
http://i.stanford.edu/pub/cstr/reports/csl/tr/89/379/CSL-TR-89-379.pdf