Reuse of formal verification efforts of incomplete models at the requirements specification stage

Even though verifying systems during any phase of the development process is a remarkable advantage of using formal techniques, in software engineering practice the great computing resources needed to verify medium-large and large systems entails an efficiency problem in incremental life-cycles, where each iteration implies identifying new requirements, verifying them and, in many cases, modifying the current release of the system to satisfy the new functional specifications. In order to improve the consistency checking process in this kind of life-cycles, we propose reusing formal verification information - previously obtained by a model. checking algorithm - to reduce the amount of verifications. This proposal is supported by ARIFS methodology (Approximate Retrieval of Incomplete and Formal Specifications) which provides a classification mechanism and an approximate and efficient retrieval one (without formal proofs) to recover the verification information linked to formal and incomplete functional specifications.