Automatic Runtime Consistency Checking and Debugging of Formally Specified Programs
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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 programs 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.
- Computer Programming and Software