Advertisement

Vacuum Cleaning CTL Formulae

Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2404)

Abstract

Vacuity detection in model checking looks for properties that hold in a model, and can be strengthened without causing them to fail. Such properties often signal problems in the model, its environment, or the properties themselves. The seminal paper of Beer et al. [1] proposed an efficient algorithm applicable to a restricted set of properties. Subsequently, Kupferman and Vardi [15] extended vacuity detection to more expressive specification mechanisms. They advocated a more minute examination of temporal logic formulae than the one adopted in [1]. However, they did not address the issues of practicality and usefulness of this more scrupulous inspection. In this paper we discuss efficient algorithms for the detection of vacuous passes of temporal logic formulae, showing that a thorough vacuity check for CTL formulae can be carried out with very small overhead, and even, occasionally, in less time than plain model checking. We also demonstrate the usefulness of such a careful analysis with the help of case studies.

Keywords

Model Check Parse Tree Atomic Proposition Automatic Test Pattern Generation Fairness Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full conference paper text

References

  1. [1]
    I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. In O. Grumberg, editor, Ninth Conference on Computer Aided Verification (CAV’97), pages 279–290. Springer-Verlag, Berlin, 1997. LNCS 1254.Google Scholar
  2. [2]
    R. Bloem, K. Ravi, and F. Somenzi. Efficient decision procedures for model checking of linear time logic properties. In N. Halbwachs and D. Peled, editors, Eleventh Conference on Computer Aided Verification (CAV’99), pages 222–235. Springer-Verlag, Berlin, 1999. LNCS 1633.Google Scholar
  3. [3]
    R. Bloem, K. Ravi, and F. Somenzi. Symbolic guided search for CTL model checking. In Proceedings of the Design Automation Conference, pages 29–34, Los Angeles, CA, June 2000.Google Scholar
  4. [4]
    R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV’96), pages 428–432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.Google Scholar
  5. [5]
    R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.Google Scholar
  6. [6]
    H. Chockler, O. Kupferman, R. P. Kurshan, and M. Y. Vardi. A practical approach to coverage in model checking. In G. Berry, H. Comon, and A. Finkel, editors, Thirteenth Conference on Computer Aided Verification (CAV’01), pages 66–78. Springer-Verlag, Berlin, July 2001. LNCS 2102.Google Scholar
  7. [7]
    H. Chockler, O. Kupferman, and M. Y. Vardi. Coverage metrics for temporal logic model checking. In Tools and algorithms for the construction and analysis of systems (TACAS), pages 528–542. Springer, 2001. LNCS 2031.CrossRefGoogle Scholar
  8. [8]
    E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings Workshop on Logics of Programs, pages 52–71, Berlin, 1981. Springer-Verlag. LNCS 131.CrossRefGoogle Scholar
  9. [9]
    E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.Google Scholar
  10. [10]
    O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using Boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111–128, Leuven, Belgium, November 1989.Google Scholar
  11. [11]
    E. W. Dijkstra. Cooperating sequential processes. In Genuys, editor, Programming Languages, pages 43–112. Academic Press, 1968.Google Scholar
  12. [12]
    H. Fujiwara. Logic Testing and Design for Testability. MIT Press, Cambridge, MA, 1985.Google Scholar
  13. [13]
    Y. Hoskote, T. Kam, P.-H. Ho, and X. Zhao. Coverage estimation for symbolic model checking. In Proceedings of the Design Automation Conference, pages 300–305, New Orleans, LA, June 1999.Google Scholar
  14. [14]
    S. Katz, O. Grumberg, and D. Geist. “Have I written enough properties?” — A method of comparison between specification and implementation. In Correct Hardware Design and Verification Methods (CHARME’99), pages 280–297, Berlin, September 1999. Springer-Verlag. LNCS 1703.Google Scholar
  15. [15]
    O. Kupferman and M. Y. Vardi. Vacuity detection in temporal model checking. In Correct Hardware Design and Verification Methods (CHARME’99), pages 82–96, Berlin, September 1999. Springer-Verlag. LNCS 1703.Google Scholar
  16. [16]
    R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.Google Scholar
  17. [17]
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.Google Scholar
  18. [18]
    K. Ravi and F. Somenzi. Hints to accelerate symbolic traversal. In Correct Hardware Design and Verification Methods (CHARME’99), pages 250–264, Berlin, September 1999. Springer-Verlag. LNCS 1703.Google Scholar
  19. [19]
    D. Verkest, L. Claesen, and H. De Man. Special benchmark session on formal system design. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 75–76, Leuven, Belgium, November 1989.Google Scholar
  20. [20]

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  1. 1.University of Colorado at BoulderUSA

Personalised recommendations

Cite paper