Structure Based Formal Methods for Software Engineering

It is widely recognized that the cost of software is far out stripping that of hardware, and that software repair, improvement, and enhancement typically consume the major portion of the cost. There are several reasons for the high cost of modification. Research on rapid prototyping is expected to help in this regard. Another reason is that a system implementation may not meet its requirements. Approaches to this problem include testing, formal verification, and runtime assertion checking. However, the dominant source of cost is system modification, which is necessitated by changes in requirements and in the support environment. If the design or the implementation of a large system is changed,the incremental cost of an individual change can be unacceptably high because a seemingly minor change to one part of a system can have unforeseen and subtle consequences in another part. Some changes always will have far-reaching effects.The root cause is the implementation goal of good performance which usually dominates and conflicts with the goals of maintaining clarity and structure. We have devised formal techniques that can substantially reduce the cost of modifying large systems, especially those systems that have been optimized for performance. The techniques have been implemented and apply to a class of sequential systems containing such objects as modules, procedures, and variables. The ways in which objects can be related is limited at present, reducing design and implementation flexibility. We believe that our results can be generalized to handle powerful parameterization mechanisms, object-oriented paradigms, and concurrency. However, this has not yet been done.