Relating counterexamples to test cases in CTL model checking specifications

ABSTRACT

Counterexamples produced by model checkers are frequently exploited for the purpose of testing. Counterexamples and test cases are generally treated as essentially the same thing, while in fact they can differ significantly. For example, it might take more than one test case to "cover" a given counterexample, because not all property violations can be illustrated with linear counterexamples. This paper presents a formal relationship between counterexamples and test cases in the context of the Computation Tree Logic (CTL), the logic of the popular model checker SMV. Given a test requirement as a CTL formula, we define what it means for a set of test cases to cover a counterexample associated with that requirement. This result can not only be used in the generation of a test set that satisfies a given test coverage criterion, but also in the determination of whether an extant test set satisfies the criterion. Our results can guide the production of counterexamples in model checkers explicitly intended to support testing.

REFERENCES

• 1: A. Abdurazik, Evaluation of Three Specification-Based Testing Criteria, Proceedings of the 6th IEEE International Conference on Complex Computer Systems, p.179, September 11-15, 2000
• 2: Paul Ammann , Paul E. Black, A Specification-Based Coverage Metric to Evaluate Test Sets, The 4th IEEE International Symposium on High-Assurance Systems Engineering, p.239-248, November 17-19, 1999
• 3: Daling Xu, Using a Model Checker to Test Safety Properties, Proceedings of the Seventh International Conference on Engineering of Complex Computer Systems, p.212, June 11-13, 2001
• 4: Paul E. Ammann , Paul E. Black , William Majurski, Using Model Checking to Generate Tests from Specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.46, December 09-11, 1998
• 5: J. Callahan, F. Schneider, and S. Easterbrook. Automated Software Testing Using Model-Checking. In Proceedings 1996 SPIN Workshop, August 1996. Also WVU Technical Report NASA-IVV-96-022.
• 6: J. J. Chilenski and S. P. Miller. Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, pages 193--200, September 1994.
• 7: E. Clarke and H. Veith. Counterexamples revisited: Principles, algorithms, applications. In Verification: Theory and Practice, volume 2772 of Lecture Notes in Computer Science, pages 208--224, 2004.
• 8: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 9: E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.427-432, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217565]
• 10: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA., 1 edition, 2001. 3rd printing.
• 11: Edmund M. Clarke , Somesh Jha , Yuan Lu , Helmut Veith, Tree-Like Counterexamples in Model Checking, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.19-29, July 22-25, 2002
• 12: E. Allen Emerson , Joseph Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.169-180, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802190]
• 13: André Engels , Loe M. G. Feijs , Sjouke Mauw, Test Generation for Intelligent Networks Using Model Checking, Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.384-398, April 02-04, 1997
• 14: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.146-162, September 06-10, 1999, Toulouse, France
• 15: K. L. McMillan. The SMV system. Technical Report CMU-CS-92-131, Carnegie-Mellon University, 1992.
• 16: I. L. Li Tan, Oleg Sokolsky. Specification-based testing with linear temporal logic. In Proceedings of IEEE International Conference on Information Reuse and Integration (IRI'04), pages 493--498, 2004.
• 17: R. Meolic, A. Fantechi, and S. Gnesi. Witness and counterexample automata for actl. In Formal Techniques for Networked and Distributed Systems - FORTE 2004, volume 3235 of Lecture Notes in Computer Science, pages 259--275, 2004.
• 18: A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, 31 October-2 November, Providence, Rhode Island, USA, pages 46--57. IEEE, 1977.
• 19: C. Ramakrishnan and R. Sekar. Model-based vulnerability analysis of computer systems. In Proceedings of the 2nd International Workshop on Verification, Model Checking and Abstract Interpretation, September 1998.
• 20: S. Rayadurgam and M. P. Heimdahl. Generating MC/DC Adequate Test Sequences Through Model Checking. In Proceedings of the 28th Annual NASA Goddard Software Engineering Workshop, pages 91--96, 2003.
• 21: S. Rayadurgam and M. P. E. Heimdahl. Coverage Based Test-Case Generation Using Model Checkers. In Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001), pages 83--91, Washington, DC, April 2001. IEEE Computer Society.
• 22: Ronald W. Ritchey , Paul Ammann, Using Model Checking to Analyze Network Vulnerabilities, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.156, May 14-17, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Measurement, Theory

Keywords:
counterexamples, formal methods, model checking, software testing, state machines, test coverage criteria