Advertisement

Improving the Consistency Checking Process by Reusing Formal Verification Knowledge

  • Rebeca P. Díaz Redondo
  • José J. Pazos Arias
  • Ana Fernández Vilas
  • Jorge García Duque
  • Alberto Gil Solla
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alpern, B., Schneider, F.B.: Recognizing Safety and Liveness. Distributed Computing Journal 2, 117–126 (1987)zbMATHCrossRefGoogle Scholar
  2. 2.
    Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  3. 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. 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. 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. 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
  7. 7.
    Lam, W., McDermid, J.A., Vickers, A.J.: Ten Steps Towards Systematic Requirements Reuse. Requirements Engineering 2, 102–113 (1997)CrossRefGoogle Scholar
  8. 8.
    McMillan, K.L.: A Technique of State Space Search based on Unfolding. Formal Methods in System Design 6, 45–65 (1995)zbMATHCrossRefGoogle Scholar
  9. 9.
    Arias, J.J.P., Duque, J.G.: SCTL-MUS: A Formal Methodology for Software Development of Distributed Systems. A Case Study. Formal Aspects of Computing 13, 50–91 (2001)zbMATHCrossRefGoogle Scholar
  10. 10.
    Penix, J., Alexander, P.: Efficient Specification-Based Component Retrieval. Automated Software Engineering: An International Journal 6(2), 139–170 (1999)CrossRefGoogle Scholar
  11. 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. 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
  13. 13.
    Zaremski, A.M., Wing, J.M.: Specification Matching of Software Components. ACM Transactions on Software Engineering and Methodology 6(4), 333–369 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Rebeca P. Díaz Redondo
    • 1
  • José J. Pazos Arias
    • 1
  • Ana Fernández Vilas
    • 1
  • Jorge García Duque
    • 1
  • Alberto Gil Solla
    • 1
  1. 1.Departamento de Enxeñería TelemáticaUniversidade de VigoVigoSpain

Personalised recommendations