What causes a system to satisfy a specification?

ABSTRACT

Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. Coverage metrics attempt to check which parts of a system are actually relevant for the verification process to succeed. Recent work on coverage in model checking suggests several coverage metrics and algorithms for finding parts of the system that are not covered by the specification. The work has already proven to be effective in practice, detecting design errors that escape early verification efforts in industrial settings. In this article, we relate a formal definition of causality given by Halpern and Pearl to coverage. We show that it gives significant insight into unresolved issues regarding the definition of coverage and leads to potentially useful extensions of coverage. In particular, we introduce the notion of responsibility, which assigns to components of a system a quantitative measure of their relevance to the satisfaction of the specification.

REFERENCES

• 1: Ammann, P. and Black, P. 2001. A specification-based coverage metric to evaluate test sets. Int. J. Qual. Reliabil. Safety Eng. 8, 4, 275--300.
• 2: Derek L. Beatty , Randal E. Bryant, Formally verifying a microprocessor using a simulation methodology, Proceedings of the 31st annual conference on Design automation, p.596-602, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196575]
• 3: Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in ACTL Formulas, Proceedings of the 9th International Conference on Computer Aided Verification, p.279-290, June 22-25, 1997
• 4: Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in Temporal Model Checking, Formal Methods in System Design, v.18 n.2, p.141-163, March 1, 2001 [doi>10.1023/A:1008779610539]
• 5: J. M. Bieman , D. Dreilinger , Lijun Lin, Using fault injection to increase software test coverage, Proceedings of the The Seventh International Symposium on Software Reliability Engineering (ISSRE '96), p.166, October 30-November 02, 1996
• 6: Budd, T. 1981. Mutation analysis: Ideas, examples, problems, and prospects. In Computer Program Testing. B. Chandrasekaran and S. Radichi, Eds. North-Holland, Amsterdam, The Netherlands, 129--148.
• 7: Budd, T. and Angluin, D. 1982. Two notions of correctness and their relation to testing. Acta Informatica 18, 31--45.
• 8: Chockler, H. and Halpern, J. Y. 2004. Responsibility and blame: A structural-model approach. J. Art. Intell. Res. 22, 93--115.
• 9: Hana Chockler , Orna Kupferman, Coverage of Implementations by Simulating Specifications, Proceedings of the IFIP 17th World Computer Congress - TC1 Stream / 2nd IFIP International Conference on Theoretical Computer Science: Foundations of Information Technology in the Era of Networking and Mobile Computing, p.409-421, August 25-30, 2002
• 10: Hana Chockler , Orna Kupferman , Robert P. Kurshan , Moshe Y. Vardi, A Practical Approach to Coverage in Model Checking, Proceedings of the 13th International Conference on Computer Aided Verification, p.66-78, July 18-22, 2001
• 11: Hana Chockler , Orna Kupferman , Moshe Y. Vardi, Coverage Metrics for Temporal Logic Model Checking, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.528-542, April 02-06, 2001
• 12: Chockler, H., Kupferman, O., and Vardi, M. 2003. Coverage metrics for formal verification. In Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science, vol. 2860. Springer-Verlag, Berlin, Germany, 111--125.
• 13: 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]
• 14: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 15: R. A. DeMillo , R. J. Lipton , F. G. Sayward, Hints on Test Data Selection: Help for the Practicing Programmer, Computer, v.11 n.4, p.34-41, April 1978 [doi>10.1109/C-M.1978.218136]
• 16: David L. Dill, What's between simulation and formal verification? (extended abstract), Proceedings of the 35th annual conference on Design automation, p.328-329, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277138]
• 17: Eiter, T. and Lukasiewicz, T. 2002a. Causes and explanations in the structural-model approach: tractable cases. In Proceedings of the 18th Conference on Uncertainty in Artificial Intelligence (UAI 2002). 146--153.
• 18: Thomas Eiter , Thomas Lukasiewicz, Complexity results for structure-based causality, Artificial Intelligence, v.142 n.1, p.53-89, November 2002
• 19: Emerson, E. and Clarke, E. 1982. Using branching time logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241--266.
• 20: Alex Groce , Sagar Chaki , Daniel Kroening , Ofer Strichman, Error explanation with distance metrics, International Journal on Software Tools for Technology Transfer (STTT), v.8 n.3, p.229-247, June 2006 [doi>10.1007/s10009-005-0202-0]
• 21: Hall, N. 2004. Two concepts of causation. In Causation and Counterfactuals. J. Collins, N. Hall, and L. A. Paul Eds. MIT Press, Cambridge, MA.
• 22: Halpern, J. Y. and Pearl, J. 2005. Causes and explanations: A structural-model approach. Part I: Causes. British J. Philos. Sci. 56, 4, 843--887.
• 23: Yatin Hoskote , Timothy Kam , Pei-Hsin Ho , Xudong Zhao, Coverage estimation for symbolic model checking, Proceedings of the 36th ACM/IEEE conference on Design automation, p.300-305, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309936]
• 24: Hume, D. 1739. A Treatise of Human Nature. John Noon, London, U.K.
• 25: Nikhil Jayakumar , Mitra Purandare , Fabio Somenzi, Dos and don'ts of CTL state coverage estimation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775908]
• 26: Mark W. Krentel, The complexity of optimization problems, Journal of Computer and System Sciences, v.36 n.3, p.490-509, June 1988 [doi>10.1016/0022-0000(88)90039-6]
• 27: Orna Kupferman , Moshe Y. Vardi, Vacuity Detection in Temporal Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.82-96, September 27-29, 1999
• 28: Kupferman, O. and Vardi, M. 2003. Vacuity detection in temporal model checking. J. Softw. Tools Techn. Transf. 4, 2, 224--233.
• 29: Orna Kupferman , Moshe Y. Vardi , Pierre Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), v.47 n.2, p.312-360, March 2000 [doi>10.1145/333979.333987]
• 30: Kurshan, R. 1998. FormalCheck User's Manual. Cadence Design, Inc., San Jose, CA.
• 31: Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 32: R. A. DeMillo , R. J. Lipton , F. G. Sayward, Hints on Test Data Selection: Help for the Practicing Programmer, Computer, v.11 n.4, p.34-41, April 1978 [doi>10.1109/C-M.1978.218136]
• 33: Richard A. DeMillo , A. Jefferson Offutt, Constraint-Based Automatic Test Data Generation, IEEE Transactions on Software Engineering, v.17 n.9, p.900-910, September 1991 [doi>10.1109/32.92910]
• 34: Christos H. Papadimitriou, On the complexity of unique solutions, Journal of the ACM (JACM), v.31 n.2, p.392-400, April 1984 [doi>10.1145/62.322435]
• 35: Papadimitriou, C. H. 1994. Computational Complexity, 2nd ed. Addison-Wesley, Reading, MA.
• 36: Doron A. Peled , David Gries , Fred B. Schneider, Software reliability methods, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 37: Mitra Purandare , Fabio Somenzi, Vacuum Cleaning CTL Formulae, Proceedings of the 14th International Conference on Computer Aided Verification, p.485-499, July 27-31, 2002
• 38: Hong Zhu , Patrick A. V. Hall , John H. R. May, Software unit test coverage and adequacy, ACM Computing Surveys (CSUR), v.29 n.4, p.366-427, Dec. 1997 [doi>10.1145/267580.267590]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.4 Knowledge Representation Formalisms and Methods
          Subjects: Relation systems

Keywords:
Model checking, causality, coverage metrics, responsibility