Improving the Consistency Checking Process by Reusing Formal Verification Knowledge
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.
Unable to display preview. Download preview PDF.
- 3.Redondo, R.P.D., Arias, J.J.P., Vilas, A.F., Martínez, B.B.: ARIFS: an Environment for Incomplete and Formal Specifications Reuse. In: Proc. of Workshop on Formal Methods and Component Interaction. Electronic Notes in Theorethical Computer Science, vol. 66. Elsevier Science, Amsterdam (July 2002)Google Scholar
- 4.Redondo, R.P.D., Arias, J.J.P., Vilas, A.F.: Component-Based Software Quality: Methods and Techniques. Lecture Notes in Computer Science (LNCS), ch. Reuse of Formal Verification Efforts of Incomplete Models at the Requirements Specification Stage, vol. 2693, pp. 326–352. Springer, Heidelberg (2003)CrossRefGoogle Scholar
- 5.Keidar, I., Khazan, R., Lynch, N., Shvartsman, A.: An Inheritance-Based Technique for Building Simulation Proofs Incrementally. In: 22nd International Conference on Software Engineering (ICSE), Limerik, Ireland, June 2000, pp. 478–487 (2000)Google Scholar
- 6.Kurshan, R., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static Partial Order Reduction. In: Tools for the Construction and Analysis of Systems. LNCS, vol. 1394, pp. 345–357 (1998)Google Scholar
- 11.Schumann, J., Fischer, B.: NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical. In: Proc. of the 12th ASE, pp. 246–254 (1997)Google Scholar
- 12.van Glabeek, R.J.: Handbook of Process Algebra. chapter The Linear Time - Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes. Elsevier Science, Amsterdam (2001)Google Scholar