Abstract
The automated generation of graph models has become an enabler in several testing scenarios, including the testing of modeling environments used in the design of critical systems, or the synthesis of test contexts for autonomous vehicles. Those approaches rely on the automated construction of consistent graph models, where each model satisfies complex structural properties of the target domain captured in first-order logic predicates. In this paper, we propose a transformation technique to map such graph generation tasks to a problem consisting of first-order logic formulae, which can be solved by state-of-the-art TPTP-compliant theorem provers, producing valid graph models as outputs. We conducted performance measurements over all 73 theorem provers available in the TPTP library, and compared our approach with other solver-based approaches like Alloy and VIATRA Solver.
Chapter PDF
Similar content being viewed by others
References
Viatra solver project. https://github.com/viatra/VIATRA-Generator
Ali, S., Iqbal, M.Z., Khalid, M., Arcuri, A.: Improving the performance of OCL constraint solving with novel heuristics for logical operations: a search-based approach. Empirical Software Engineering 21(6), 2459–2502 (Dec 2016). https://doi.org/10.1007/s10664-015-9392-6
Atkinson, T., Plump, D., Stepney, S.: Evolving graphs by graph programming. In: Genetic Programming - 21st European Conference, EuroGP 2018, Parma, Italy, April 4-6, 2018, Proceedings. LNCS, vol. 10781, pp. 35–51. Springer (2018). https://doi.org/10.1007/978-3-319-77553-1_3
Atkinson, T., Plump, D., Stepney, S.: Evolving graphs with horizontal gene transfer. In: Proceedings of the Genetic and Evolutionary Computation Conference, GECCO 2019, Prague, Czech Republic, July 13-17, 2019. pp. 968–976. ACM (2019). https://doi.org/10.1145/3321707.3321788
Bagan, G., Bonifati, A., Ciucanu, R., Fletcher, G.H.L., Lemay, A., Advokaat, N.: gmark: Schema-driven generation of graphs and queries. IEEE Trans. Knowl. Data Eng. 29(4), 856–869 (2017). https://doi.org/10.1109/TKDE.2016.2633993
Brucker, A.D., Wolff, B.: HOL-OCL: A formal proof environment for UML/OCL. In: Fiadeiro, J.L., Inverardi, P. (eds.) Fundamental Approaches to Software Engineering. pp. 97–100. Springer, Berlin, Heidelberg (2008)
Büttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: ICFEM. pp. 198–213. Springer (2012)
Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. Journal of Systems and Software (Mar 2014). https://doi.org/10.1016/j.jss.2014.03.023
Gogolla, M., Büttner, F., Richters, M.: USE: A UML-based specification environment for validating UML and OCL. Science of Computer Programming 69(1), 27 – 34 (2007). https://doi.org/10.1016/j.scico.2007.01.013
González Pérez, C.A., Buettner, F., Clarisó, R., Cabot, J.: EMFtoCSP: A Tool for the Lightweight Verification of EMF Models. In: Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA). Zurich, Switzerland (Jun 2012), https://hal.inria.fr/hal-00688039
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA (1993)
Hao, W.: Automated metamodel instance generation satisfying quantitative constraints. Ph.D. thesis, National University of Ireland Maynooth (2013)
Jackson, D.: Alloy: a lightweight object modelling notation. Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002). https://doi.org/10.1145/505145.505149
Jackson, D.: Software Abstractions: logic, language, and analysis. MIT press (2012)
Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Model Driven Engineering Languages and Systems, pp. 653–667. Springer (2011)
Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain specific modeling languages. In: EMSOFT. pp. 53–62. ACM, New York, NY, USA (2006)
Juneau, J.: Object Relational Mapping and JPA, pp. 55–72. Apress, Berkeley, CA (2013)
Khurshid, S., Marinov, D.: Testera: Specification-based testing of java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004). https://doi.org/10.1023/B:AUSE.0000038938.10589.b9
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044. pp. 1–35. CAV 2013, Springer-Verlag, New York, NY, USA (2013)
Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: A tool for generating structurally complex test inputs. In: ICSE. pp. 771–774. IEEE Computer Society (2007). https://doi.org/10.1109/ICSE.2007.48
Miller, J.F.: Cartesian genetic programming: its status and future. Genetic Programming and Evolvable Machines (2019). https://doi.org/10.1007/s10710-019-09360-6
de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. pp. 337–340 (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Navarro, J.A., Voronkov, A.: Proof systems for effectively propositional logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning. pp. 426–440. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)
The Object Management Group: Object Constraint Language, v2.4 (February 2014)
Schneider, S., Lambers, L., Orejas, F.: Symbolic model generation for graph properties. In: Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. pp. 226–243 (2017). https://doi.org/10.1007/978-3-662-54494-5_13
Schneider, S., Lambers, L., Orejas, F.: Automated reasoning for attributed graph properties. STTT 20(6), 705–737 (2018). https://doi.org/10.1007/s10009-018-0496-3
Semeráth, O., Babikian, A.A., Pilarski, S., Varró, D.: VIATRA Solver: a framework for the automated generation of consistent domain-specific models. In: ICSE. pp. 43–46 (2019), https://dl.acm.org/citation.cfm?id=3339687
Semeráth, O., Barta, Á., Horváth, Á., Szatmári, Z., Varró, D.: Formal validation of domain-specific languages with derived features and well-formedness constraints. Software and Systems Modeling pp. 357–392 (2017). https://doi.org/10.1016/j.entcs.2008.04.038
Semeráth, O., Farkas, R., Bergmann, G., Varró, D.: Diversity of graph models and graph generators in mutation testing. STTT 22(1), 57–78 (2020). https://doi.org/10.1007/s10009-019-00530-6
Semeráth, O., Nagy, A.S., Varró, D.: A graph solver for the automated generation of consistent domain-specific models. In: ICSE. pp. 969–980. ACM (2018). https://doi.org/10.1145/3180155.3180186
Soltana, G., Sabetzadeh, M., Briand, L.C.: Synthetic data generation for statistical testing. In: ASE. pp. 872–882 (2017). https://doi.org/10.1109/ASE.2017.8115698
Soltana, G., Sabetzadeh, M., Briand, L.C.: Practical model-driven data generation for system testing. CoRR abs/1902.00397 (2019)
Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automated Reasoning 59(4), 483–502 (Dec 2017). https://doi.org/10.1007/s10817-017-9407-7
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: TACAS. LNCS, vol. 4424, pp. 632–647. Springer (2007). https://doi.org/10.1007/978-3-540-71209-1_49
Ujhelyi, Z., Bergmann, G., Hegedüs, Á., Horváth, Á., Izsó, B., Ráth, I., Szatmári, Z., Varró, D.: EMF-IncQuery: An integrated development environment for live model queries. Sci. Comput. Program. 98, 80–99 (2015). https://doi.org/10.1016/j.scico.2014.01.004
Varró, D., Bergmann, G., Hegedüs, Á., Horváth, Á., Ráth, I., Ujhelyi, Z.: Road to a reactive and incremental model transformation platform: three generations of the VIATRA framework. Software and Systems Modeling 15(3), 609–629 (2016)
Varró, D., Semeráth, O., Szárnyas, G., Horváth, Á.: Towards the automated generation of consistent, diverse, scalable and realistic graph models. In: Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig. LNCS, vol. 10800, pp. 285–312. Springer (2018). https://doi.org/10.1007/978-3-319-75396-6_16
Wu, H., Monahan, R., Power, J.F.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: TASE. pp. 175–182 (July 2013). https://doi.org/10.1109/TASE.2013.31
Yakindu Statechart Tools: Yakindu (2019), http://statecharts.org/
Acknowledgements
The first author was partially supported by the Fonds de recherche du Québec - Nature et technologies (FRQNT) B1X scholarship (file number: 272709). This paper is partially supported by MTA-BME Lendület Research Group on Cyber-Physical Systems, and NSERC RGPIN-04573-16 project.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Babikian, A.A., Semeráth, O., Varró, D. (2020). Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers. In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)