Tearing based automatic abstraction for CTL model checking

ABSTRACT

In this paper we present the tearing paradigm as a way to automatically abstract behavior to obtain upper and lower bound approximations of a reactive system. We present algorithms that exploit the bounds to perform conservative ECTL and ACTL model checking. We also give an algorithm for false negative (or false positive) resolution for verification based on a theory of a lattice of approximations. We show that there exists a bipartition of the lattice set based on positive versus negative verification results. Our resolution methods are based on determining a pseudo-optimal shortest path from a given, possibly coarse but tractable approximation, to a nearest point on the contour separating one set of the bipartition from the other.

REFERENCES

• 1: Felice Balarin , Alberto L. Sangiovanni-Vincentelli, An Iterative Approach to Language Containment, Proceedings of the 5th International Conference on Computer Aided Verification, p.29-40, June 28-July 01, 1993
• 2: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 3: Jerry R. Burch, Using BDDs to verify multipliers, Proceedings of the 28th conference on ACM/IEEE design automation, p.408-412, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127703]
• 4: H. Cho and F. Somenzi. Sequential logic optimization based on state space decomposition. In Proceedings of the European Conference on Design Automation, pages 200-204, Paris, France, February 1993.
• 5: P. Kelb, D. Dams, and R. Gerth. Practical symbolic model checking of the full /~-calculus using compositional abstractions. Technical Report 95-31, Department of Computing Science, Eindhoven University of Technology, 1995.
• 6: David E. Long , Anca Browne , Edmund M. Clarke , Somesh Jha , Wilfredo R. Marrero, An Improved Algorithm for the Evaluation of Fixpoint Expressions, Proceedings of the 6th International Conference on Computer Aided Verification, p.338-350, June 21-23, 1994
• 7: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 8: R. Milner. An algebraic definition of simulation between programs. Proc. 2nd Int. Joint Co@ on Artificial Intelligence, pages 481-489, 1971.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Sequential circuits

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.2 Reliability and Testing**
          Subjects: Test generation**
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Design, Theory, Verification

Keywords:
ACTL model checking, CTL model checking, bipartition, conservative ECTL, formal verification, lattice set, lower bound approximations, pseudo-optimal shortest path, reactive system, resolution methods, tearing based automatic abstraction, upper bound approximations