Top

Published in:

2020 | OriginalPaper | Chapter

Diverse Scenario Exploration in Model Finders Using Graph Kernels and Clustering

Authors : Robert Clarisó, Jordi Cabot

Published in: Rigorous State-Based Methods

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Complex software systems can be described using modeling notations such as UML/OCL or Alloy. Then, some correctness properties of these systems can be checked using model finders, which compute sample scenarios either fulfilling the desired properties or illustrating potential faults. Such scenarios allow designers to validate, verify and test the system under development.

Nevertheless, when asked to produce several scenarios, model finders tend to produce similar solutions. This lack of diversity impairs their effectiveness as testing or validation assets. To solve this problem, we propose the use of graph kernels, a family of methods for computing the (dis)similarity among pairs of graphs. With this metric, it is possible to cluster scenarios effectively, improving the usability of model finders and making testing and validation more efficient.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Adding Concurrency to a Sequential Refinement Tower

next chapter Formal Verification of Interoperability Between Future Network Architectures Using Alloy

The intermediate vertex is omitted when the position i can be inferred: no other position in the relation has a compatible signature, i.e., with a common supertype.

Graphs \(G_1=(V_1,E_1)\) and \(G_2=(V_2,E_2)\) are called isomorphic if there is a mapping \(f: V_1 \rightarrow V_2\) such that \(\forall x, y \in V_1: (x,y) \in E_1 \text { iff } (f(x),f(y)) \in E_2\).

https://github.com/AlloyTools/models.

https://igraph.org.

https://cran.r-project.org/package=graphkernels.

https://cran.r-project.org/package=cluster.

Ali, S., Zohaib Iqbal, M., Arcuri, A., Briand, L.C.: Generating test data from OCL constraints with search techniques. IEEE Trans. Softw. Eng. 39(10), 1376–1402 (2013). https://doi.org/10.1109/TSE.2013.17

Batot, E., Sahraoui, H.: A generic framework for model-set selection for the unification of testing and learning MDE tasks. In: ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (MODELS 2016), pp. 374–384. ACM Press, New York (2016). https://doi.org/10.1145/2976767.2976785

Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014). https://doi.org/10.1016/j.jss.2014.03.023

Cadavid, J.J., Baudry, B., Sahraoui, H.: Searching the boundaries of a modeling space to test metamodels. In: IEEE International Conference on Software Testing, Verification and Validation (ICST 2012), pp. 131–140. IEEE (2012). https://doi.org/10.1109/ICST.2012.93

Dutra, R., Laeufer, K., Bachrach, J., Sen, K.: Efficient sampling of SAT solutions for testing. In: International Conference on Software Engineering (ICSE 2018), pp. 549–559. ACM (2018). https://doi.org/10.1145/3180155.3180248

Ferdjoukh, A., Galinier, F., Bourreau, E., Chateau, A., Nebut, C.: Measurement and generation of diversity and meaningfulness in model driven engineering. Int. J. Adv. Softw. 11(1/2), 131–146 (2018). https://hal-lirmm.ccsd.cnrs.fr/lirmm-02067506

Ghosh, S., Das, N., Gonçalves, T., Quaresma, P., Kundu, M.: The journey of graph kernels through two decades. Comput. Sci. Rev. 27, 88–111 (2018). https://doi.org/10.1016/J.COSREV.2017.11.002

González, C.A., Cabot, J.: Formal verification of static software models in MDE: a systematic review. Inf. Softw. Technol. 56(8), 821–838 (2014). https://doi.org/10.1016/j.infsof.2014.03.003

Hilken, F., Gogolla, M., Burgueño, L., Vallecillo, A.: Testing models and model transformations using classifying terms. Softw. Syst. Modeling 17(3), 885–912 (2016). https://doi.org/10.1007/s10270-016-0568-3CrossRef

10.

Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006). https://mitpress.mit.edu/books/software-abstractions

11.

Jackson, E.K., Simko, G., Sztipanovits, J.: Diversely enumerating system-level architectures. In: International Conference on Embedded Software (EMSOFT 2013), pp. 1–10. IEEE, September 2013. https://doi.org/10.1109/EMSOFT.2013.6658589

12.

Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 290–306. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21952-8_21CrossRef

13.

Li, G., Semerci, M., Yener, B., Zaki, M.J.: Effective graph classification based on topological and label attributes. Stat. Anal. Data Mining 5(4), 265–283 (2012). https://doi.org/10.1002/sam.11153MathSciNetCrossRef

14.

Mougenot, A., Darrasse, A., Blanc, X., Soria, M.: Uniform random generation of huge metamodel instances. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol. 5562, pp. 130–145. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02674-4_10CrossRef

15.

Nadel, A.: Generating diverse solutions in SAT. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 287–301. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_23CrossRefMATH

16.

Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: International Conference on Software Engineering (ICSE 2013), pp. 232–241. IEEE, May 2013. https://doi.org/10.1109/ICSE.2013.6606569

17.

Petre, M.: UML in practice. In: International Conference on Software Engineering (ICSE 2013), pp. 722–731. IEEE Press (2013). https://doi.org/10.1109/ICSE.2013.6606618

18.

Plazar, Q., Acher, M., Perrouin, G., Devroey, X., Cordy, M.: Uniform sampling of SAT solutions for configurable systems: are we there yet? In: IEEE Conference on Software Testing, Validation and Verification (ICST 2019), pp. 240–251. IEEE (2019). https://doi.org/10.1109/ICST.2019.00032

19.

Rousseeuw, P.J.: Silhouettes: a graphical aid to the interpretation and validation of cluster analysis. J. Comput. Appl. Math. 20(1), 53–65 (1987). https://doi.org/10.1016/0377-0427(87)90125-7CrossRefMATH

20.

Semeráth, O., Nagy, A.S., Varró, D.: A graph solver for the automated generation of consistent domain-specific models. In: International Conference on Software Engineering (ICSE 2018), pp. 969–980. ACM Press (2018). https://doi.org/10.1145/3180155.3180186

21.

Semeráth, O., Varró, D.: Iterative generation of diverse models for testing specifications of DSL tools. In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 227–245. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89363-1_13CrossRef

22.

Shervashidze, N., Schweitzer, P., van Leeuwen, E.J., Mehlhorn, K., Borgwardt, K.M.: Weisfeiler-Lehman graph kernels. J. Mach. Learn. Res. 12, 2539–2561 (2001). https://dl.acm.org/citation.cfm?id=2078187

23.

Soltana, G., Sabetzadeh, M., Briand, L.C.: Synthetic data generation for statistical testing. In: IEEE/ACM International Conference on Automated Software Engineering (ASE 2017), pp. 872–882. IEEE (2017). https://doi.org/10.1109/ASE.2017.8115698

24.

Soltana, G., Sabetzadeh, M., Briand, L.C.: Practical model-driven data generation for system testing. ACM Transactions on Software Engineering and Methodology (2020, to appear). http://arxiv.org/abs/1902.00397

25.

Vadlamudi, S.G., Kambhampati, S.: A combinatorial search perspective on diverse solution generation. In: AAAI Conference on Artificial Intelligence, pp. 776–783. AAAI Press (2016). https://dl.acm.org/citation.cfm?id=3015927

26.

Varró, D., Semeráth, O., Szárnyas, G., Horváth, Á.: Towards the automated generation of consistent, diverse, scalable and realistic graph models. In: Heckel, R., Taentzer, G. (eds.) Graph Transformation, Specifications, and Nets. LNCS, vol. 10800, pp. 285–312. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75396-6_16CrossRefMATH

27.

Vishwanathan, S., Schraudolph, N.N., Kondor, R., Borgwardt, K.M.: Graph kernels. J. Mach. Learn. Res. 11(Apr), 1201–1242 (2010). http://www.jmlr.org/papers/v11/vishwanathan10a.html

28.

Wu, H.: MaxUSE: a tool for finding achievable constraints and conflicts for inconsistent UML class diagrams. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 348–356. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_23CrossRef

29.

Xu, R., Wunsch, D.: Survey of clustering algorithms. IEEE Trans. Neural Netw. 16(3), 645–678 (2005). https://doi.org/10.1109/TNN.2005.845141

Title: Diverse Scenario Exploration in Model Finders Using Graph Kernels and Clustering
Authors: Robert Clarisó
Jordi Cabot
Publisher: Springer International Publishing
Book: Rigorous State-Based Methods
Print ISBN: 978-3-030-48076-9

Electronic ISBN: 978-3-030-48077-6

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-48077-6_3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner