Report Number: CSL-TR-90-436
Institution: Stanford University, Computer Systems Laboratory
Title: Application of formal specification to software maintenance
Author: Madhav, Neel
Author: Sankar, Sriram
Date: August 1990
Abstract: This paper describes the use of formal specifications and associated tools in addressing various aspects of software maintenance ---corrective, perfective, and adaptive. It also addresses the refinement of the software development process to build programs that are easily maintainable. The task of software maintenance in our case includes the task of maintaining the specification as well as maintaining the program. We focus on the use of Anna, a specification language for formally specifying Ada programs, to aid us in maintaining Ada programs. These techniques are applicable to most other specification language and programming language environments. The tools of interest are: (1) the Anna Specification Analyzer which allows us to analyze the specification for correctness with respect to our informal understanding of program behavior; and (2) the Anna Consistency Checking System which monitors the Ada program at runtime based on the Anna specification.
http://i.stanford.edu/pub/cstr/reports/csl/tr/90/436/CSL-TR-90-436.pdf