Automatic Runtime Consistency Checking and Debugging of Formally Specified Programs
Abstract
This thesis studies an approach to automate the process of deciding whether a program is performing correctly, and if not, to discover the probable cause of the problem. It assumes that the intended program's behavior is specified in some formal, high-level specification language. It studies how one can check automatically at runtime whether the program is running consistently with its specification, and if not, how inconsistencies can be automatically detected and diagnosed. A method of using this checking method for debugging formally specified programs is then presented. The consistency checking method depends on the particular specification language constructs used. This thesis studies two categories of constructs: 1) generalized assertions and 2) algebraic specifications. Generalized assertions contain boolean expressions that must be satisfied within a specified region in the underlying program. Checking functions are generated which test for the truth of these boolean expressions. Diagnostic messages are given and a debugger is invoked if there is a violation. Checking functions are called from locations in the program where the specification may have changed value. In this thesis, algebraic specifications are considered to be equations whose terms comprise abstract data type operations. Algebraic specification checking involves monitoring the execution of the abstract data type operations. Based on this monitoring and the algebraic specifications, a theorem prover generates invariants that the program must satisfy. If the program does not satisfy these invariants, diagnostic messages are given and a debugger is invoked.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1989
- Accession Number
- ADA218855
Entities
People
- Sriram Sankar
Organizations
- Stanford University