Management of Change in Structured Verification




Change


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. But 
any change of a specification either by 
adding new parts or by changing erroneous 
parts affects existing verification work in a 
subtle way. In this paper 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 datastructure 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.