Skip to main content
SpringerLink
Log in

Verifying Controllability of Time-Aware Business Processes

  • Conference paper
  • First Online:
Rules and Reasoning (RuleML+RR 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10364))

Included in the following conference series:

Abstract

We present an operational semantics for time-aware business processes, that is, processes modeling the execution of business activities, whose durations are subject to linear constraints over the integers. We assume that some of the durations are controllable, that is, they can be determined by the organization that enacts the process, while others are uncontrollable, that is, they are determined by the external world.

Then, we consider controllability properties, which guarantee the completion of the enactment of the process, satisfying the given duration constraints, independently of the values of the uncontrollable durations. Controllability properties are encoded by quantified reachability formulas, where the reachability predicate is recursively defined by a set of Constrained Horn Clauses (CHCs). These clauses are automatically derived from the operational semantics of the process.

Finally, we present two algorithms for solving the so called weak and strong controllability problems. Our algorithms reduce these problems to the verification of a set of quantified integer constraints, which are simpler than the original quantified reachability formulas, and can effectively be handled by state-of-the-art CHC solvers.

This work has been partially funded by INdAM-GNCS (Italy). E. De Angelis, F. Fioravanti, and A. Pettorossi are research associates at IASI-CNR, Rome, Italy.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In WC we introduce a small optimization by using a query that avoids obtaining multiple answers with the same values of U.

  2. 2.

    The experiments have been performed on an Intel Core Duo E7300 2.66 Ghz processor with 4GB of memory under GNU/Linux OS.

References

  1. van der Aalst, W.M.P.: The application of Petri nets to workflow management. J. Circ. Syst. Comput. 8(1), 21–66 (1998)

    Google Scholar 

  2. 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 2013), pp. 163–174. ACM (2013)

    Google Scholar 

  3. Berthomieu, B., Vernadat, F.: Time Petri nets analysis with TINA. In: Proceedings of QEST 2006, pp. 123–124. IEEE Computer Society (2006)

    Google Scholar 

  4. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015). doi:10.1007/978-3-319-23534-9_2

    Chapter  Google Scholar 

  5. Cheikhrouhou, S., Kallel, S., Guermouche, N., Jmaiel, M.: The temporal perspective in business process modeling: a survey and research challenges. Serv. Oriented Comput. Appl. 9(1), 75–85 (2015)

    Google Scholar 

  6. Cimatti, A., Hunsberger, L., Micheli, A., Posenato, R., Roveri, M.: Dynamic controllability via timed game automata. Acta Informatica 53(6), 681–722 (2016)

    Google Scholar 

  7. Cimatti, A., Micheli, A., Roveri, M.: Solving strong controllability of temporal problems with uncertainty using SMT. Constraints 20(1), 1–29 (2015)

    Google Scholar 

  8. Cimatti, A., Micheli, A., Roveri, M.: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty. Artif. Intell. 224, 1–27 (2015)

    Google Scholar 

  9. Combi, C., Posenato, R.: Controllability in temporal conceptual workflow schemata. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 64–79. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03848-8_6

    Chapter  Google Scholar 

  10. Damaggio, E., Deutsch, A., Vianu, V.: Artifact systems with data dependencies and arithmetic. ACM Trans. Database Syst. 37(3), 1–36 (2012)

    Google Scholar 

  11. De Angelis, E., Fioravanti, F., Meo, M.C., Pettorossi, A., Proietti, M.: Verification of time-aware business processes using Constrained Horn Clauses. In: Preliminary Proceedings of LOPSTR 2016, CoRR. http://arxiv.org/abs/1608.02807 (2016)

  12. De Angelis, E., Fioravanti, F., Meo, M.C., Pettorossi, A., Proietti, M.: Verifying controllability of time-aware business processes. Technical report IASI-CNR 16-08 (2016)

    Google Scholar 

  13. Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: a tool for verifying programs through transformations. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 568–74. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_47

    Chapter  Google Scholar 

  14. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions by program specialization. In: Proceedings of the PPDP 2015, pp. 91–102. ACM (2015)

    Google Scholar 

  15. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  16. Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theor. Comput. Sci. 166, 101–146 (1996)

    Google Scholar 

  17. Formal Systems (Europe) Ltd. Failures-Divergences Refinement, FDR2 User Manual (1998). http://www.fsel.com

  18. ter Hofstede, A.M., van der Aalst, W.M.P., Adams, M., Russell, N. (eds.): Modern Business Process Automation: YAWL and its Support Environment. Springer, Heidelberg (2010)

    Google Scholar 

  19. Jaffar, J., Maher, M.: Constraint logic programming: a survey. J. Logic Program. 19(20), 503–81 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  20. Kowalski, R.A., Sergot, M.J.: A logic-based calculus of events. New Gener. Comput. 4(1), 67–95 (1986)

    Article  MATH  Google Scholar 

  21. Kumar, A., Sabbella, S.R., Barton, R.R.: Managing controlled violation of temporal process constraints. In: Motahari-Nezhad, H.R., Recker, J., Weidlich, M. (eds.) BPM 2015. LNCS, vol. 9253, pp. 280–96. Springer, Cham (2015). doi:10.1007/978-3-319-23063-4_20

    Chapter  Google Scholar 

  22. Lanz, A., Posenato, R., Combi, C., Reichert, M.: Controlling time-awareness in modularized processes. In: Schmidt, R., Guédria, W., Bider, I., Guerreiro, S. (eds.) BPMDS/EMMSAD -2016. LNBIP, vol. 248, pp. 157–72. Springer, Cham (2016). doi:10.1007/978-3-319-39429-9_11

    Google Scholar 

  23. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)

    Google Scholar 

  24. Makni, M., Tata, S., Yeddes, M., Ben Hadj-Alouane, N.: Satisfaction and coherence of deadline constraints in inter-organizational workflows. In: Meersman, R., Dillon, T., Herrero, P. (eds.) OTM 2010. LNCS, vol. 6426, pp. 523–39. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16934-2_39

    Chapter  Google Scholar 

  25. McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 4, pp. 463–502. Edinburgh University Press (1969)

    Google Scholar 

  26. OMG. Business Process Model and Notation. http://www.omg.org/spec/BPMN/

  27. Peintner, B., Venable, K.B., Yorke-Smith, N.: Strong controllability of disjunctive temporal problems with uncertainty. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 856–63. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_64

    Chapter  Google Scholar 

  28. Proietti, M., Smith, F.: Reasoning on data-aware business processes with constraint logic. In: Proceedings of the SIMPDA 2014. CEUR, vol. 1293, pp. 60–75 (2014)

    Google Scholar 

  29. Smith, F., Proietti, M.: Rule-based behavioral reasoning on semantic business processes. In: Proceedings of the ICAART 2013, vol. II, pp. 130–143. SciTePress (2013)

    Google Scholar 

  30. Thielscher, M.: From Situation Calculus to Fluent Calculus: State update axioms as a solution to the inferential frame problem. Artif. Intell. 111(1-2), 277–299 (1999)

    Google Scholar 

  31. Venable, K.B., Volpato, M., Peintner, B., Yorke-Smith, N.: Weak and dynamic controllability of temporal problems with disjunctions and uncertainty. In: Proceedings of the COPLAS 2010, pp. 50–59 (2010)

    Google Scholar 

  32. Vidal, T., Fargier, H.: Handling contingency in temporal constraint networks: from consistency to controllabilities. J. Exp. Theor. Artif. Intell. 11(1), 23-45 (1999)

    Google Scholar 

  33. Watahiki, K., Ishikawa, F., Hiraishi, K.: Formal verification of business processes with temporal and resource constraints. In: Proceedings of the SMC 2011, pp. 1173–1180. IEEE (2011)

    Google Scholar 

  34. Weber, I., Hoffmann, J., Mendling, J.: Beyond soundness: on the verification of semantic business process models. Distrib. Parallel Databases 27, 271–343 (2010)

    Google Scholar 

  35. Weske, M.: Business Process Management: Concepts, Languages, Architectures. Springer, Heidelberg (2007)

    Google Scholar 

  36. Wong, P.Y.H., Gibbons, J.: A relative timed semantics for BPMN. Electron. Notes Theor. Comput. Sci. 229(2), 59–75 (2009)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DEC, University ‘G. D’Annunzio’, Pescara, Italy

    Emanuele De Angelis, Fabio Fioravanti & Maria Chiara Meo

  2. DICII, University of Rome Tor Vergata, Rome, Italy

    Alberto Pettorossi

  3. IASI-CNR, Rome, Italy

    Maurizio Proietti

Authors
  1. Emanuele De Angelis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabio Fioravanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maria Chiara Meo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Emanuele De Angelis or Maurizio Proietti .

Editor information

Editors and Affiliations

  1. University of L’Aquila, L’Aquila, Italy

    Stefania Costantini

  2. Free University of Bozen-Bolzano, Bolzano, Italy

    Enrico Franconi

  3. Dalhousie University, Halifax, Nova Scotia, Canada

    William Van Woensel

  4. Birkbeck, University of London, London, United Kingdom

    Roman Kontchakov

  5. Imperial College London, London, United Kingdom

    Fariba Sadri

  6. SINTEF/University of Oslo, Oslo, Norway

    Dumitru Roman

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

De Angelis, E., Fioravanti, F., Meo, M.C., Pettorossi, A., Proietti, M. (2017). Verifying Controllability of Time-Aware Business Processes. In: Costantini, S., Franconi, E., Van Woensel, W., Kontchakov, R., Sadri, F., Roman, D. (eds) Rules and Reasoning. RuleML+RR 2017. Lecture Notes in Computer Science(), vol 10364. Springer, Cham. https://doi.org/10.1007/978-3-319-61252-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-61252-2_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-61251-5

  • Online ISBN: 978-3-319-61252-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation