Synthesis of Infinite-State Abstractions and Their Use for Software Validation

  • Carlo Ghezzi
  • Andrea Mocci
  • Mario Sangiorgio
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


In the recent years, several research efforts have been devoted to developing approaches to synthesize specifications of software behavior. Most of the proposed approaches addressed the inference of finite-state abstractions. The synthesized abstractions have been integrated in different validation scenarios, such as testing. While finite-state models can be effectively used as models of a software component’s behavior for certain specific purposes, they can hardly be used as full-fledged specifications. Because of their very limited expressive power, they cannot represent some of the component behaviors and may lead to synthesizing too coarse abstractions. In this paper, we survey a set of approaches that instead infer infinite-state abstractions, which can be used to express richer sets of behaviors of a software component in a black-box manner. For such approaches, we also discuss the few existing applications to software validation. In particular, we discuss the limitations and identify how, in principle, they can be used in different validation scenarios and how this opens new research directions.


Model Check Software Component Symbolic Execution Generate Test Case Software Validation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Young, M., Pezze, M.: Software Testing and Analysis: Process, Principles and Techniques. John Wiley & Sons (2007)Google Scholar
  2. 2.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2) (1992)Google Scholar
  3. 3.
    Ernst, M.D.: Dynamically Discovering Likely Program Invariants. Ph.D. thesis, University of Washington, Seattle, Washington (August 2000)Google Scholar
  4. 4.
    Robillard, M., Bodden, E., Kawrykow, D., Mezini, M., Ratchford, T.: Automated api property inference techniques. IEEE Transactions on Software Engineering 39(5), 613–637 (2013)CrossRefGoogle Scholar
  5. 5.
    Dallmeier, V., Lindig, C., Wasylkowski, A., Zeller, A.: Mining object behavior with adabu. In: Proceedings of the 2006 International Workshop on Dynamic Systems Analysis, WODA 2006, pp. 17–24. ACM, New York (2006)CrossRefGoogle Scholar
  6. 6.
    Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A.: Generating test cases for specification mining. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA 2010, pp. 85–96. ACM, New York (2010)Google Scholar
  7. 7.
    De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S.: Program abstractions for behaviour validation. In: 2011 33rd International Conference on Software Engineering (ICSE), pp. 381–390 (2011)Google Scholar
  8. 8.
    Xie, T., Notkin, D.: Tool-assisted unit-test generation and selection based on operational abstractions. Automated Software Engineering 13(3), 345–371 (2006)CrossRefGoogle Scholar
  9. 9.
    Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX). FORTE XII / PSTV XIX 1999, pp. 225–240. Kluwer, The Netherlands (1999)Google Scholar
  10. 10.
    Mocci, A., Sangiorgio, M.: Detecting component changes at run time with behavior models. Computing 95(3), 191–221 (2013)CrossRefGoogle Scholar
  11. 11.
    Meyer, B.: Applying “Design by Contract”. IEEE Computer 25(10), 40–51 (1992)CrossRefGoogle Scholar
  12. 12.
    Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27–52 (1978), MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. Foundations of Computing Series. Mit Press (1996)Google Scholar
  14. 14.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69(1-3), 35–45 (2007); Special issue on Experimental Software and ToolkitsMathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Csallner, C., Tillmann, N., Smaragdakis, Y.: DySy: Dynamic symbolic execution for invariant inference. In: Proceedings of the 30th International Conference on Software Engineering, ICSE 2008, pp. 281–290. ACM, New York (2008)Google Scholar
  16. 16.
    Tillmann, N., Chen, F., Schulte, W.: Discovering likely method specifications. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 717–736. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Wei, Y., Furia, C.A., Kazmin, N., Meyer, B.: Inferring better contracts. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 191–200. ACM, New York (2011)Google Scholar
  18. 18.
    Alpuente, M., Feliú, M.A., Villanueva, A.: Automatic inference of specifications using matching logic. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, pp. 127–136. ACM, New York (2013)Google Scholar
  19. 19.
    Henkel, J., Reichenbach, C., Diwan, A.: Discovering documentation for Java container classes. IEEE Trans. Software Eng. 33(8), 526–543 (2007)CrossRefGoogle Scholar
  20. 20.
    Ghezzi, C., Mocci, A., Monga, M.: Efficient recovery of algebraic specifications for stateful components. In: Ninth International Workshop on Principles of Software Evolution: In Conjunction with the 6th ESEC/FSE Joint Meeting, IWPSE 2007, pp. 98–105. ACM, New York (2007)Google Scholar
  21. 21.
    Xie, T., Notkin, D.: Automatically identifying special and common unit tests for object-oriented programs. In: Proc. 16th IEEE International Symposium on Software Reliability Engineering (ISSRE 2005), pp. 277–287 (November 2005)Google Scholar
  22. 22.
    Bacci, G., Comini, M., Feliú, M.A., Villanueva, A.: Automatic synthesis of specifications for first order Curry programs. In: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming, PPDP 2012, pp. 25–34. ACM, New York (2012)Google Scholar
  23. 23.
    Ghezzi, C., Mocci, A., Monga, M.: Synthesizing intensional behavior models by graph transformation. In: IEEE 31st International Conference on Software Engineering, ICSE 2009, pp. 430–440. IEEE (2009)Google Scholar
  24. 24.
    Meyer, B.: Design by Contract: The Eiffel Method. In: International Conference on Technology of Object-Oriented Languages, p. 446 (1998)Google Scholar
  25. 25.
    Roşu, G., Ştefănescu, A.: Matching Logic: A New Program Verification Approach (NIER Track). In: ICSE 2011: Proceedings of the 30th International Conference on Software Engineering, pp. 868–871. ACM (2011)Google Scholar
  26. 26.
    Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Commun. ACM 15, 1053–1058 (1972)CrossRefGoogle Scholar
  27. 27.
    Meyer, B., Fiva, A., Ciupa, I., Leitner, A., Wei, Y., Stapf, E.: Programs that test themselves. Computer 42(9), 46–55 (2009)CrossRefGoogle Scholar
  28. 28.
    Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science 245(1), 55–101 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Comini, M., Torella, L.: A condensed goal-independent fixpoint semantics modeling the small-step behavior of rewriting. In: Kovacs, L., Kutsia, T. (eds.) SCSS 2013. EPiC Series, vol. 15, pp. 31–49. EasyChair (2013)Google Scholar
  30. 30.
    Janicki, R., Sekerinski, E.: Foundations of the trace assertion method of module interface specification, vol. 27, pp. 577–598. IEEE Press, Piscataway (2001)Google Scholar
  31. 31.
    Bartussek, W., Parnas, D.L.: Using assertions about traces to write abstract specifications for software modules. In: Bracchi, G., Lockemann, P. (eds.) Information Systems Methodology. LNCS, vol. 65, pp. 211–236. Springer, Heidelberg (1978)Google Scholar
  32. 32.
    Parnas, D.L.: A technique for software module specification with examples. Commun. ACM 15(5), 330–336 (1972)CrossRefGoogle Scholar
  33. 33.
    Ernst, M.: Daikon-related invariant detection publications (2013),
  34. 34.
    Csallner, C., Smaragdakis, Y., Xie, T.: DSD-Crasher: A hybrid analysis tool for bug finding. ACM Trans. Softw. Eng. Methodol. 17(2), 8:1–8:37 (2008)CrossRefGoogle Scholar
  35. 35.
    Wei, Y., Roth, H., Furia, C., Pei, Y., Horton, A., Steindorfer, M., Nordio, M., Meyer, B.: Stateful testing: Finding more errors in code and contracts. In: 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 440–443 (2011)Google Scholar
  36. 36.
    Xie, T., Notkin, D.: Mutually enhancing test generation and specification inference. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 60–69. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  37. 37.
    Ghezzi, C., Mocci, A., Salvaneschi, G.: Automatic cross validation of multiple specifications: A case study. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 233–247. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  38. 38.
    Silva, L.S., Wei, Y., Meyer, B., Oriol, M.: Evotec: Evolving the best testing strategy for contract-equipped programs. In: APSEC, pp. 290–297 (2011)Google Scholar
  39. 39.
    Doong, R.K., Frankl, P.G.: The astoot approach to testing object-oriented programs. ACM Transactions on Software Engineering and Methodology 3(2), 101–130 (1994)CrossRefGoogle Scholar
  40. 40.
    Xie, T., Marinov, D., Notkin, D.: Rostra: A framework for detecting redundant object-oriented unit tests. In: 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pp. 196–205 (2004)Google Scholar
  41. 41.
    Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  42. 42.
    Baresi, L., Di Nitto, E., Ghezzi, C.: Toward open-world software: Issues and challenges. IEEE Computer 39(10), 36–43 (2006)CrossRefGoogle Scholar
  43. 43.
    Bianculli, D., Ghezzi, C.: Monitoring conversational web services. In: 2nd International Workshop on Service Oriented Software Engineering: in Conjunction with the 6th ESEC/FSE Joint Meeting, IW-SOSWE 2007, pp. 15–21. ACM, New York (2007)CrossRefGoogle Scholar
  44. 44.
    Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J.M., Irwin, J.: Aspect-oriented programming. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  45. 45.
    Henkel, J., Reichenbach, C., Diwan, A.: Developing and debugging algebraic specifications for java classes. ACM Trans. Softw. Eng. Methodol. 17(3), 14:1–14:37 (2008)CrossRefGoogle Scholar
  46. 46.
    Diaconescu, R., Futatsugi, K., Iida, S.: Component-based algebraic specification and verification in CafeOBJ. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1644–1663. Springer, Heidelberg (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Carlo Ghezzi
    • 1
  • Andrea Mocci
    • 1
  • Mario Sangiorgio
    • 1
  1. 1.Dipartimento di Elettronica, Informazione e BioingegneriaPolitecnico di MilanoMilanoItaly

Personalised recommendations