Regresar

Improving the consistency checking process by reusing formal verification knowledge

Abstract:

At an iterative and incremental requirements capture stage, each iteration implies identifying new requirements, checking their with the current functional specification of the system, and, in many cases, modifying this global specification to satisfy them. In a totally formalized environment, these verifications are usually done applying a model checking algorithm which entails the well-known efficiency problems to check medium-large and large systems. In order to reduce the amount of verifications and, consequently these efficiency problems, we propose reusing previously obtained formal verification results. The ARIFS methodology (Approximate Retrieval of Incomplete and Formal Specifications) supports the classification and the efficient retrieval (without formal proofs) of the verification information stored in the repository and, in this paper, we show how to carry out this proposal by using an application example. © Springer-Verlag Berlin Heidelberg 2003.