nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

From Model Completeness to Verification of Data Aware Processes

verfasst von : Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin

Erschienen in: Description Logic, Theory Combination, and All That

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Model Completeness is a classical topic in model-theoretic algebra, and its inspiration sources are areas like algebraic geometry and field theory. Yet, recently, there have been remarkable applications in computer science: these applications range from combined decision procedures for satisfiability and interpolation, to connections between temporal logic and monadic second order logic and to model-checking. In this paper we mostly concentrate on the last one: we study verification over a general model of so-called artifact-centric systems, which are used to capture business processes by giving equal important to the control-flow and data-related aspects. In particular, we are interested in assessing (parameterized) safety properties irrespectively of the initial database instance. We view such artifact systems as array-based systems, establishing a correspondence with model checking based on Satisfiability-Modulo-Theories (SMT). Model completeness comes into the picture in this framework by supplying quantifier elimination algorithms for suitable existentially closed structures. Such algorithms, whose complexity is unexpectedly low in some cases of our interest, are exploited during search and to represent the sets of reachable states. Our first implementation, built up on top of the mcmt model-checker, makes all our foundational results fully operational and quite effective, as demonstrated by our first experiments.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel The What-To-Ask Problem for Ontology-Based Peers

Nächstes Kapitel Situation Calculus Meets Description Logics

http://smtlib.cs.uiowa.edu/.

It is quite curious to notice that this observation (in its essence) was already present in the paper [45], where however model completeness was not mentioned at all! Instead of quantifier elimination in the model completion \(T^*\), the authors of [45] relied on the computation of the so called ‘cover’ of an existential formula (such cover turns out to be equivalent to the quantifier free equivalent formula modulo \(T^*\)).

Again, without mentioning any specific application, this was already observed in [45], as the specialization of the cover algorithm to signatures with unary free function symbols.

For the purposes of this definition, we may equivalently take the formula to be quantifier-free.

Arity and source/target sorts for F can be deduced from the context (considering that everything is well-typed).

This directly implies that \(\phi \) is satisfiable also in a DB instance that interprets value sorts into finite sets.

By ‘signature’ we always mean ‘signature with equality’, so as soon as new sorts are added, the corresponding equality predicates are added too.

In accordance with mcmt conventions, we denote the application of an artifact component a to a term (i.e., constant or variable) v also as a[v] (standard notation for arrays), instead of a(v).

Recall that \(a_j =\lambda y. d_{j}\) abbreviates \(\forall y\, a_{j}(y)=d_{j}\).

Non-deterministic updates can be formalized using existentially quantified variables in the transition.

This is unrelated to cyclicity of \(\varSigma \) defined in Sect. 3, and comes from universal algebra terminology.

http://users.mat.unimi.it/users/ghilardi/mcmt/, subdirectory /examples/dbdriven of the distribution. The user manual contains a new section (pages 36–39) on how to encode RAS s in MCMT specifications.

http://www.bpmn.org/.

Abdulla, P.A., Aiswarya, C., Atig, M.F., Montali, M., Rezine, O.: Recency-bounded verification of dynamic database-driven systems. In: Proceedings of the PODS, pp. 195–210 (2016)

Alberti, F., Armando, A., Ranise, S.: ASASP: automated symbolic analysis of security policies. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 26–33. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_4CrossRef

Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 679–685. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_49CrossRef

Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014)CrossRef

Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Brief announcement: automated support for the design and validation of fault tolerant parameterized systems - a case study. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol. 6343, pp. 392–394. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15763-9_36CrossRef

Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. J. Satisfiability Boolean Model. Comput. 8(1/2), 29–61 (2012)

Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 18–23. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6_2CrossRefMATH

Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinite-state systems. Fundam. Inf. 150(1), 1–24 (2017)MathSciNetCrossRef

Baader, F., Ghilardi, S.: Connecting many-sorted structures and theories through adjoint functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 31–47. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_2CrossRef

10.

Baader, F., Ghilardi, S.: Connecting many-sorted theories. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 278–294. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_21CrossRef

11.

Baader, F., Ghilardi, S.: Connecting many-sorted theories. J. Symbolic Logic 72(2), 535–583 (2007)MathSciNetCrossRef

12.

Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Inf. Comput. 204(10), 1413–1452 (2006)MathSciNetCrossRef

13.

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRef

14.

Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Inf. Comput. 178(2), 346–390 (2002)MathSciNetCrossRef

15.

Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., Montali, M.: Verification of relational data-centric dynamic systems with external services. In: Proceedings of the PODS, pp. 163–174 (2013)

16.

Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proceedings of the KR (2012)

17.

Bojańczyk, M., Segoufin, L., Toruńczyk, S.: Verification of database-driven systems via amalgamation. In: Proceedings of the PODS, pp. 63–74 (2013)

18.

Bruschi, D., Di Pasquale, A., Ghilardi, S., Lanzi, A., Pagani, E.: Formal verification of ARP (address resolution protocol) through SMT-based model checking - a case study. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 391–406. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_26CrossRef

19.

Bruttomesso, R., Carioni, A., Ghilardi, S., Ranise, S.: Automated analysis of parametric timing-based mutual exclusion algorithms. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 279–294. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_28CrossRef

20.

Calvanese, D. ., De Giacomo, G., Montali, M.: Foundations of data aware process analysis: a database theory perspective. In: Proceedings of the PODS, pp. 1–12 (2013)

21.

Calvanese, D., De Giacomo, G., Montali, M., Patrizi, F.: First-order mu-calculus over generic transition systems and applications to the situation calculus. Inf. Comput. 259, 328–347 (2017)CrossRef

22.

Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness for the verification of data-aware processes. Manuscript submitted for publication (2018)

23.

Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Quantifier elimination for database driven verification. Technical report arXiv:1806.09686, arXiv.org (2018)

24.

Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes via array-based systems (extended version). Technical report arXiv:1806.11459, arXiv.org (2018)

25.

Carioni, A., Ghilardi, S., Ranise, S.: MCMT in the land of parametrized timed automata. In: Proceedings of the VERIFY. EPiC Series in Computing, vol. 3, pp. 47–64 (2010)

26.

Chang, C.-C., Keisler, J.H.: Model Theory. North-Holland Publishing Co. (1990)

27.

Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_55CrossRef

28.

Damaggio, E., Deutsch, A., Vianu, V.: Artifact systems with data dependencies and arithmetic. ACM TODS 37(3), 22 (2012)CrossRef

29.

Damaggio, E., Hull, R., Vaculín, R.: On the equivalence of incremental and fixpoint semantics for business artifacts with Guard-Stage-Milestone lifecycles. Inf. Syst. 38(4), 561–584 (2013)CrossRef

30.

Delzanno, G., Podelski, A., Esparza, J.: Constraint-based analysis of broadcast protocols. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 50–66. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48168-0_5CrossRef

31.

Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proceedings of the ICDT, pp. 252–267. ACM (2009)

32.

Deutsch, A., Li, Y., Vianu, V.: Verification of hierarchical artifact systems. In: Proceedings of the PODS, pp. 179–194 (2016)

33.

Dumas, M.: On the convergence of data and process engineering. In: Eder, J., Bielikova, M., Tjoa, A.M. (eds.) ADBIS 2011. LNCS, vol. 6909, pp. 19–26. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23737-9_2CrossRef

34.

Dutertre, B., De Moura, L.: The YICES SMT solver. Technical report, SRI International (2006)

35.

Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of the LICS, pp. 352–359. IEEE Computer Society (1999)

36.

Fiorentini, C., Ghilardi, S.: Combining word problems through rewriting in categories with products. TCS 294(1–2), 103–149 (2003)MathSciNetCrossRef

37.

Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. JAR 33(3–4), 221–249 (2004)MathSciNetCrossRef

38.

Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (the non-disjoint signatures case). In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 316–332. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_18CrossRef

39.

Ghilardi, S., Gianola, A.: Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Logic 169(8), 731–754 (2018)MathSciNetCrossRef

40.

Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67–82. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_6CrossRef

41.

Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4) (2010)

42.

Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_3CrossRef

43.

Ghilardi, S., van Gool, S.J.: Monadic second order logic as the model companion of temporal logic. In: Proceedings of the LICS, pp. 417–426. ACM (2016)

44.

Ghilardi, S., van Gool, S.J.: A model-theoretic characterization of monadic second order logic on infinite words. J. Symbolic Logic 82(1), 62–76 (2017)MathSciNetCrossRef

45.

Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 193–207. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78739-6_16CrossRefMATH

46.

Hull, R.: Artifact-centric business process models: brief survey of research results and challenges. In: Meersman, R., Tari, Z. (eds.) OTM 2008. LNCS, vol. 5332, pp. 1152–1163. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88873-4_17CrossRef

47.

Kruskal, J.B.: Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture. Trans. Amer. Math. Soc. 95, 210–225 (1960)MathSciNetMATH

48.

Künzle, V., Weber, B., Reichert, M.: Object-aware business processes: fundamental requirements and their support in existing approaches. Int. J. Inf. Syst. Model. Des. 2(2), 19–46 (2011)CrossRef

49.

Kutz, O., Lutz, C., Wolter, F., Zakharyaschev, M.: E-connections of abstract description systems. AIJ 156(1), 1–73 (2004)MathSciNetMATH

50.

Li, Y., Deutsch, A., Vianu, V.: VERIFAS: a practical verifier for artifact systems. PVLDB 11(3), 283–296 (2017)

51.

Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245–257 (1979)CrossRef

52.

Pigozzi, D.: The join of equational theories. Colloq. Math. 30, 15–25 (1974)MathSciNetCrossRef

53.

Reichert, M.: Process and data: two sides of the same coin? In: Meersman, R., et al. (eds.) OTM 2012. LNCS, vol. 7565, pp. 2–19. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33606-5_2CrossRef

54.

Richardson, C.: Warning: don’t assume your business processes use master data. In: Hull, R., Mendling, J., Tai, S. (eds.) BPM 2010. LNCS, vol. 6336, pp. 11–12. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15618-2_3CrossRef

55.

Robinson, A.: On the Metamathematics of Algebra. North-Holland (1951)

56.

Robinson, A.: Introduction to model theory and to the metamathematics of algebra. In: Studies in Logic and the Foundations of Mathematics. North-Holland (1963)

57.

Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 5–24. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40184-8_2CrossRef

58.

Silver, B.: BPMN Method and Style. 2nd edn. Cody-Cassidy (2011)

59.

Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 273–289. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_19CrossRef

60.

Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3) (2018)

61.

Tinelli, C., Harandi, M.: A new correctness proof of the nelson-oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. ALS, vol. 3, pp. 103–119. Springer, Dordrecht (1996). https://doi.org/10.1007/978-94-009-0349-4_5CrossRefMATH

62.

Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: Proceedings of the ICDT, pp. 1–13. ACM (2009)

63.

Wolter, f.: Fusions of modal logics revisited. In: Advances in Modal Logic. CSLI Lecture Notes, vol. 1, pp. 361–379 (1996)

Titel: From Model Completeness to Verification of Data Aware Processes
verfasst von: Diego Calvanese
Silvio Ghilardi
Alessandro Gianola
Marco Montali
Andrey Rivkin
Verlag: Springer International Publishing
Buch: Description Logic, Theory Combination, and All That
Print ISBN: 978-3-030-22101-0

Electronic ISBN: 978-3-030-22102-7

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-22102-7_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner