Reuse of Verificatino Efforts and Incomplete Specifications in a Formalized, Iterative and Incremental Software Process

Abstract

The possibility of verifying systems during any phase of the software development process is one of the most significant advantages of using formal methods. Model checking is considered to be the broadest-used formal verification technique, even though a great quantity of computing resources are needed to verify medium-large and large systems. As verification is present over the whole software process, this amount of resources is more critical in incremental and iterative life-cycles. Our proposal focuses on reusing incomplete models and their verification results - which are obtained from a model-checking algorithm - in order to improve this kind of life-cycle. Making good use of these previous verification results can reduce the formal verification costs by minimizing the set of requirements and the set of system states where the properties must be verified. The unspecification that is inherent to incomplete systems is used to provide an approximate and content-oriented retrieval which is supplemented by suggestions to match the desired specifications.