Abstract
Various tools for program analysis, including run-time assertion checkers and static analyzers such as verification and test generation tools, require formal specifications of the programs being analyzed. Moreover, many of these tools and techniques require such specifications to be written in a particular style, or follow certain patterns, in order to obtain an acceptable performance from the corresponding analyses. Thus, having a formal specification sometimes is not enough for using a particular technique, since such specification may not be provided in the right formalism. In this paper, we deal with this problem in the increasingly common case of having an operational specification, while for analysis reasons requiring a declarative specification. We propose an evolutionary approach to translate an operational specification written in a sequential programming language, into a declarative specification, in relational logic. We perform experiments on a benchmark of data structure implementations, that show that translating representation invariants using our approach and verifying invariant preservation using the resulting specifications outperforms verification with specifications obtained using an existing semantics-preserving translation. Also, our evolutionary computation translation achieves very good precision in this context.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bicarregui, J., Bishop, M., Dimitrakos, T., Lano, K., Maibaum, T., Matthews, B., Ritchie, B.: Supporting co-use of VDM and B by translation. In: Proceedings of VDM in 2000! (2nd VDM workshop) (2000)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2002. ACM (2002)
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212–232 (2005). Springer
Cranen, S., Groote, J.F., Reniers, M.: A linear translation from CTL* to the first-order modal mu-calculus. Theor. Comput. Sci. 412(28), 3129–3139 (2011). Elsevier
Demasi, R., Castro, P.F., Maibaum, T.S.E., Aguirre, N.: Synthesizing masking fault-tolerant systems from deontic specifications. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 163–177. Springer, Heidelberg (2013). doi:10.1007/978-3-319-02444-8_13
Emerson, E.A., Samanta, R.: An algorithmic framework for synthesis of concurrent programs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 522–530. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_41
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. Sci. Comput. Program. 69(1–3), 35–45 (2007). Elsevier
Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Proceedings of International Conference on Software Engineering, ICSE 2005. ACM (2015)
Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA 2010. ACM (2010)
Galeotti, J.P., Rosner, N., Pombo, C.L., Frias, M.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283–1307 (2013). IEEE
Galeotti, J.P., Furia, C.A., May, E., Fraser, G., Zeller, A.: Inferring loop invariants by mutation, dynamic analysis, and static checking. IEEE Trans. Softw. Eng. 41(10), 1019–1037 (2015). IEEE
Ghezzi, C., Jazayeri, M., Mandiroli, D.: Fundamentals of Software Engineering, 2nd edn. Prentice-Hall, Upper Saddle River (2003)
Goldberg, D.: Genetic Algorithms in Search, Optimization and Machine Learning. Addison-Wesley, Salt Lake City (1989)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)
Web site of the Java Genetic Algorithms Package (JGAP). http://jgap.sourceforge.net
Klein, U., Piterman, N., Pnueli, A.: Effective synthesis of asynchronous systems from GR(1) specifications. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 283–298. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27940-9_19
Home Page of the Korat test generation tool. http://korat.sourceforge.net
Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_26
Liskov, B., Guttag, J.: Program Development in Java: Abstraction, Specification, and Object-Oriented Desig. Addison-Wesley, Salt Lake City (2000)
Michalewicz, Z.: Genetic Algorithms + Data Structures = Evolution Programs, Springer, Heidelberg (1996)
Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: Proceedings of the 29th International Conference on Software Engineering, ICSE 2007. IEEE (2007)
Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175–205 (2008). Springer
Ponzio, P., Aguirre, N., Frias, M., Visser, W.: Field-exhaustive testing. In: Proceedings of International Symposium on the Foundations of Software Engineering FSE 2016, Seattle (WA), USA. ACM (2016, to appear)
Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice-Hall, Upper Saddle River (2003)
Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Softw. Eng. 35(3), 384–406 (2009). IEEE
Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004. ACM (2004)
Acknowledgements
The authors would like to thank the anonymous referees for their helpful comments. This work was partially supported by the Argentinian Agency for Scientific and Technological Promotion (ANPCyT), through grants PICT 2012 No. 1298, PICT 2013 No. 2624 and PICT 2013 No. 0080.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Molina, F. et al. (2016). An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications. In: Ribeiro, L., Lecomte, T. (eds) Formal Methods: Foundations and Applications. SBMF 2016. Lecture Notes in Computer Science(), vol 10090. Springer, Cham. https://doi.org/10.1007/978-3-319-49815-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-49815-7_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-49814-0
Online ISBN: 978-3-319-49815-7
eBook Packages: Computer ScienceComputer Science (R0)