Automatic runtime consistency checking and debugging of formally specified programs
David C. Luckham, Sriram Sankar · 1989
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 behavior of the program 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 methodology of using this checking methodology for debugging formally specified programs is then presented. The consistency checking methodology depends on the particular specification language constructs used. In this thesis, two categories of constructs are studied: (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. For the purpose of 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. The theorem prover has to be specialized so that it operates efficiently in the context of algebraic specification checking. Methodologies to achieve this using incremental techniques are presented in this thesis. Based on these ideas, a working system has been built for automatic runtime consistency checking of Ada programs with specifications written in Anna. Experiments with this system has led to the development of a methodology of debugging programs based on formal specifications.