Advertisement

CompoSAT: Specification-Guided Coverage for Model Finding

  • Sorawee Porncharoenwase
  • Tim Nelson
  • Shriram Krishnamurthi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

Model-finding tools like the Alloy Analyzer produce concrete examples of how a declarative specification can be satisfied. These formal tools are useful in a wide range of domains: software design, security, networking, and more. By producing concrete examples, they assist in exploring system behavior and can help find surprising faults.

Specifications usually have many potential candidate solutions, but model-finders tend to leave the choice of which examples to present entirely to the underlying solver. This paper closes that gap by exploring notions of coverage for the model-finding domain, yielding a novel, rigorous metric for output quality. These ideas are realized in the tool CompoSAT, which interposes itself between Alloy’s constraint-solving and presentation stages to produce ensembles of examples that maximize coverage.

We show that high-coverage ensembles like CompoSAT produces are useful for, among other things, detecting overconstraint—a particularly insidious form of specification error. We detail the underlying theory and implementation of CompoSAT and evaluate it on numerous specifications.

Notes

Acknowlegements

We are grateful to the developers of Alloy and Kodkod, as well as Natasha Danas and Daniel J. Dougherty for useful discussions and their work on the Amalgam tool. We also thank the anonymous reviewers for their helpful remarks. This work is partially supported by the U.S. National Science Foundation.

References

  1. 1.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press, Cambridge (2012)Google Scholar
  2. 2.
    Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: USENIX Large Installation System Administration Conference (2010)Google Scholar
  3. 3.
    Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: class diagrams analysis using alloy revisited. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 592–607. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24485-8_44CrossRefGoogle Scholar
  4. 4.
    Maoz, S., Ringert, J.O., Rumpe, B.: CDDiff: semantic differencing for class diagrams. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 230–254. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22655-7_12CrossRefGoogle Scholar
  5. 5.
    Akhawe, D., Barth, A., Lam, P., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: IEEE Computer Security Foundations Symposium (2010)Google Scholar
  6. 6.
    Maldonado-Lopez, F.A., Chavarriaga, J., Donoso, Y.: Detecting network policy conflicts using alloy. In: Ait Ameur, Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. LNCS, vol. 8477, pp. 314–317. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-43652-3_31Google Scholar
  7. 7.
    Zave, P.: Using lightweight modeling to understand Chord. ACM Comput. Commun. Rev. 42(2), 49–57 (2012)CrossRefGoogle Scholar
  8. 8.
    Ruchansky, N., Proserpio, D.: A (not) NICE way to verify the OpenFlow switch specification: formal modelling of the OpenFlow switch using Alloy. ACM Comput. Commun. Rev. 43(4), 527–528 (2013)CrossRefGoogle Scholar
  9. 9.
    Nelson, T., Ferguson, A.D., Scheer, M.J.G., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: Networked Systems Design and Implementation (2014)Google Scholar
  10. 10.
    Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: Principled scenario exploration through minimality. In: International Conference on Software Engineering (2013)Google Scholar
  11. 11.
    Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 434–449. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21401-6_30CrossRefGoogle Scholar
  12. 12.
    Cunha, A., Macedo, N., Guimarães, T.: Target oriented relational model finding. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 17–31. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54804-8_2CrossRefGoogle Scholar
  13. 13.
    Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 168–184. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66197-1_11CrossRefGoogle Scholar
  14. 14.
    Zhu, H., Hall, P.A.V., May, J.H.R.: Software unit test coverage and adequacy. ACM Comput. Surv. 29(4), 366–427 (1997)CrossRefGoogle Scholar
  15. 15.
    Alloy Team: Overconstraint–the bane of declarative modeling. http://alloy.mit.edu/alloy/tutorials/online/sidenote-overconstraint.html. Accessed 14 Aug 2017
  16. 16.
    Jackson, D.: Alloy: a language & tool for relational models. http://alloy.mit.edu/alloy/ (2016). Accessed 1 Nov 2016
  17. 17.
    Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: International Conference on Software Engineering (2015)Google Scholar
  18. 18.
    Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)zbMATHGoogle Scholar
  19. 19.
    Libkin, L.: Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-662-07003-1
  20. 20.
    Nelson, T., Danas, N., Dougherty, D.J., Krishnamurthi, S.: The power of “why” and “why not”: Enriching scenario exploration with provenance. In: Foundations of Software Engineering (2017)Google Scholar
  21. 21.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  22. 22.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24605-3_37CrossRefGoogle Scholar
  23. 23.
    Torlak, E., Chang, F.S.-H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 326–341. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-68237-0_23CrossRefGoogle Scholar
  24. 24.
    Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: International Joint Conference On Artificial Intelligence (1995)Google Scholar
  25. 25.
    McCune, W.: Mace4 reference manual and guide. CoRR cs.SC/0310055 (2003)Google Scholar
  26. 26.
    Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71209-1_49CrossRefGoogle Scholar
  27. 27.
    Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71209-1_41CrossRefzbMATHGoogle Scholar
  28. 28.
    Macedo, N., Cunha, A., Guimarães, T.: Exploring scenario exploration. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 301–315. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46675-9_20CrossRefGoogle Scholar
  29. 29.
    Montaghami, V., Rayside, D.: Bordeaux: a tool for thinking outside the box. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 22–39. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54494-5_2CrossRefGoogle Scholar
  30. 30.
    Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Principles of Knowledge Representation and Reasoning (1996)Google Scholar
  31. 31.
    Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. Disc. Appl. Math. (2007)Google Scholar
  32. 32.
    Miller, J.C., Maloney, C.J.: Systematic mistake analysis of digital computer programs. Commun. ACM 6(2), 58–63 (1963)CrossRefGoogle Scholar
  33. 33.
    Inozemtseva, L., Holmes, R.: Coverage is not strongly correlated with test suite effectiveness. In: International Conference on Software Engineering (2014)Google Scholar
  34. 34.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Programming Language Design and Implementation (PLDI) (2005)Google Scholar
  35. 35.
    Larson, E., Austin, T.: High coverage detection of input-related security faults. In: USENIX Security Symposium (2003)Google Scholar
  36. 36.
    Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Foundations of Software Engineering (2005)Google Scholar
  37. 37.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)MathSciNetCrossRefGoogle Scholar
  38. 38.
    Hoskote, Y., Kam, T., Ho, P.H., Zhao, X.: Coverage estimation for symbolic model checking. In: Design Automation Conference (1999)Google Scholar
  39. 39.
    Gopinath, D., Zaeem, R.N., Khurshid, S.: Improving the effectiveness of spectra-based fault localization using specifications. In: Automated Software Engineering (2012)Google Scholar
  40. 40.
    Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: Automated Software Engineering (2001)Google Scholar
  41. 41.
    Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: A tool for generating structurally complex test inputs. In: International Conference on Software Engineering (2007)Google Scholar
  42. 42.
    Shao, D., Khurshid, S., Perry, D.E.: Whispec: White-box testing of libraries using declarative specifications. In: Symposium on Library-Centric Software Design (2007)Google Scholar
  43. 43.
    Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: Design Automation Conference (1994)Google Scholar
  44. 44.
    Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in actl formulas. In: International Conference on Computer Aided Verification, pp. 279–290 (1997)CrossRefGoogle Scholar
  45. 45.
    Heaven, W., Russo, A.: Enhancing the Alloy analyzer with patterns of analysis. In: Workshop on Logic-based Methods in Programming Environments (2005)Google Scholar
  46. 46.
    Sullivan, A., Zaeem, R.N., Khurshid, S., Marinov, D.: Towards a test automation framework for Alloy. In: Symposium on Model Checking of Software (SPIN), pp. 113–116 (2014)Google Scholar
  47. 47.
    Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: Software Testing, Verification and Validation (ICST) (2017)Google Scholar
  48. 48.
    Saeki, T., Ishikawa, F., Honiden, S.: Automatic generation of potentially pathological instances for validating Alloy models. In: International Conference on Formal Engineering Methods (ICFEM), pp. 41–56 (2016)CrossRefGoogle Scholar
  49. 49.
    Cui, Y., Widom, J.: Practical lineage tracing in data warehouses. In: International Conference on Data Engineering (2000)Google Scholar
  50. 50.
    Buneman, P., Khanna, S., Wang-Chiew, T.: Why and where: a characterization of data provenance. In: Van den Bussche, J., Vianu, V. (eds.) ICDT 2001. LNCS, vol. 1973, pp. 316–330. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44503-X_20CrossRefGoogle Scholar
  51. 51.
    Meliou, A., Gatterbauer, W., Moore, K.F., Suciu, D.: The complexity of causality and responsibility for query answers and non-answers. Proc. VLDB Endow. 4(1), 34–45 (2010)CrossRefGoogle Scholar
  52. 52.
    Meliou, A., Gatterbauer, W., Moore, K.F., Suciu, D.: WHY SO? or WHY NO? functional causality for explaining query answers. In: VLDB workshop on Management of Uncertain Data (MUD), pp. 3–17 (2010)Google Scholar
  53. 53.
    Schwartz-Narbonne, D., Oh, C., Schäf, M., Wies, T.: VERMEER: a tool for tracing and explaining faulty C programs. In: International Conference on Software Engineering, pp. 737–740 (2015)Google Scholar
  54. 54.
    Ko, A.J., Myers, B.A.: Designing the WhyLine: a debugging interface for asking questions about program behavior. In: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, pp. 151–158. ACM (2004)Google Scholar
  55. 55.
    Ko, A.J., Myers, B.A.: Finding causes of program output with the Java Whyline. In: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, pp. 1569–1578. ACM (2009)Google Scholar
  56. 56.
    Wu, Y., Zhao, M., Haeberlen, A., Zhou, W., Loo, B.T.: Diagnosing missing events in distributed systems with negative provenance. In: Conference on Communications Architectures, Protocols and Applications (SIGCOMM), pp. 383–394. ACM (2014)Google Scholar
  57. 57.
    Chen, A., Wu, Y., Haeberlen, A., Zhou, W., Loo, B.T.: Differential provenance: better network diagnostics with reference events. In: Workshop on Hot Topics in Networks, vol. 25. ACM (2015)Google Scholar
  58. 58.
    Maier, D., Mendelzon, A.O., Sagiv, Y.: Testing implications of data dependencies. ACM Trans. Database Syst. 4(4), 455–469 (1979)CrossRefGoogle Scholar
  59. 59.
    Glass, R.L.: Persistent software errors. IEEE Trans. Softw. Eng. 7(2), 162–168 (1981)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Sorawee Porncharoenwase
    • 1
  • Tim Nelson
    • 1
  • Shriram Krishnamurthi
    • 1
  1. 1.Brown UniversityProvidenceUSA

Personalised recommendations