”Have I Written Enough Properties?” - A Method of Comparison Between Specification and Implementation

  • Sagi Katz
  • Orna Grumberg
  • Danny Geist
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


This work presents a novel approach for evaluatingthe quality of the model checkingpro cess. Given a model of a design (or implementation) and a temporal logic formula that describes a specification, model checkingde termines whether the model satisfies the specification. Assume that all specification formulas were successfully checked for the implementation. Are we sure that the implementation is correct? If the specification is incomplete, we may fail to find an error in the implementation. On the other hand, if the specification is complete, then the model checkingpro cess can be stopped without adding more specification formulas. Thus, knowingwh ether the specification is complete may both avoid missed implementation errors and save precious verification time.

The completeness of a specification with respect to a given implementation is determined as follows. The specification formula is first transformed into a tableau. The simulation preorder is then used to compare the implementation model and the tableau model. We suggest four comparison criteria, each revealinga certain dissimilarity between the implementation and the specification. If all comparison criteria are empty, we conclude that the tableau is bisimilar to the implementation model and that the specification fully describes the implementation. We also conclude that there are no redundant states in the implementation. The method is exemplified on a small hardware example. We implemented our method symbolically as an extension to SMV. The implementation involves efficient OBDD manipulations that reduce the number of OBDD variables from 4n to 2n.


Model Check Comparison Criterion Atomic Proposition Kripke Structure Implementation State 
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.


  1. 1.
    I. Beer, S. Ben-David, C. Eisner, and A. Landver. Rulebase-an industry oriented formal verification tool. In 33th Design Automation Conference, 1996. DAC.Google Scholar
  2. 2.
    E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT press, 1999. To appear.Google Scholar
  3. 3.
    O. Grumbergan and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843–871, 1994.CrossRefGoogle Scholar
  4. 4.
    T. A. Henzinger, O. Kupferman, and S. K. Rajamani. Fair simulation. In Proc. of the 7th Conference on Concurrency Theory (CONCUR’97), volume 1243 of LNCS, Warsaw, July 1997.Google Scholar
  5. 5.
    Hoskote, Kam, Ho, and Zhao. Coverage estimation for symbolic model checking. In proceedings of the 36rd Design Automation Conference (DAC’99). IEEE Computer Society Press, June 1999.Google Scholar
  6. 6.
    Z. Manna and A. Pnueli. Temporal verifications of Reactive Systems-Safety. Springer-Verlag, 1995.Google Scholar
  7. 7.
    K. L. McMillan. The SMV System DRAFT. Carnegie Mellon University, Pittsburgh, PA, 1992.Google Scholar
  8. 8.
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Press, Norwell, MA, 1993.zbMATHGoogle Scholar
  9. 9.
    R. Milner. An algebraic definition of simulation between programs. In proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 481–489, September 1971.Google Scholar
  10. 10.
    T. Filkorn. A method for symbolic verification of synchronous circuits. In D. Borrione and R. Waxman, editors, Proceedings of The Tenth International Symposium on Computer Hardware Description Languages and their Applications, IFIP WG 10.2, pages 249–259, Marseille, April 1991. North-Holland.Google Scholar
  11. 11.
    Elaine J. Weyuker and Bingchiang Jeng. Analyzing partition testing strategies. IEEE Transactions on Software Engineering, 2(17), July 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Sagi Katz
    • 1
  • Orna Grumberg
    • 1
  • Danny Geist
    • 2
  1. 1.Computer Science DepartmentHaifaIsrael
  2. 2.IBM Haifa Research Lab.HaifaIsrael

Personalised recommendations