”Have I Written Enough Properties?” - A Method of Comparison Between Specification and Implementation
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.
KeywordsModel Check Comparison Criterion Atomic Proposition Kripke Structure Implementation State
- 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.E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT press, 1999. To appear.Google Scholar
- 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.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.Z. Manna and A. Pnueli. Temporal verifications of Reactive Systems-Safety. Springer-Verlag, 1995.Google Scholar
- 7.K. L. McMillan. The SMV System DRAFT. Carnegie Mellon University, Pittsburgh, PA, 1992.Google Scholar
- 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.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.Elaine J. Weyuker and Bingchiang Jeng. Analyzing partition testing strategies. IEEE Transactions on Software Engineering, 2(17), July 1991.Google Scholar