Management of change in structured verification
Dieter Hutter · 2000
The use of formal methods in large complex applications implies the need for an evolutionary formal program development in which specification and verification phases are interleaved. Any change of a specification either by adding new parts or by changing erroneous parts affects existing verification work in a subtle way. We present a truth maintenance system for structured specification and verification. It is based on the simple but powerful notion of a development graph as an underlying data structure to represent an actual consistent state of a formal development. Based on this notion we try to minimize the consequences of changes of existing verification work.