Advertisement

Runtime Enforcement of First-Order LTL Properties on Data-Aware Business Processes

  • Riccardo De Masellis
  • Jianwen Su
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8274)

Abstract

This paper studies the following problem: given a relational data schema, a temporal property over the schema, and a process that modifies the data instances, how can we enforce the property during each step of the process execution? Temporal properties are defined using a first-order future time LTL (FO-LTL) and they are evaluated under finite and fixed domain assumptions. Under such restrictions, existing techniques for monitoring propositional formulas can be used, but they would require exponential space in the size of the domain. Our approach is based on the construction of a first-order automaton that is able to perform the monitoring incrementally and by using exponential space in the size of the property. Technically, we show that our mechanism captures the semantics of FO-LTL on finite but progressing sequences of instances, and it reports satisfaction or dissatisfaction of the property at the earliest possible time.

Keywords

data-aware business processes runtime monitoring formal verification 

References

  1. 1.
    Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)Google Scholar
  2. 2.
    Basin, D., Klaedtke, F., Müller, S.: Policy monitoring in first-order temporal logic. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 1–18. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for ltl and tltl. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)Google Scholar
  4. 4.
    Belardinelli, F., Lomuscio, A., Patrizi, F.: Verification of deployed artifact systems via data abstraction. In: Kappel, G., Maamar, Z., Motahari-Nezhad, H.R. (eds.) ICSOC 2011. LNCS, vol. 7084, pp. 142–156. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  5. 5.
    Bhattacharya, K., Gerede, C., Hull, R., Liu, R., Su, J.: Towards formal analysis of artifact-centric business process models. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 288–304. Springer, Heidelberg (2007), http://www.springerlink.com/content/w31j312311x6310j CrossRefGoogle Scholar
  6. 6.
    Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Transactions on Database Systems 20(2), 149–186 (1995)CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    Damaggio, E., Deutsch, A., Hull, R., Vianu, V.: Automatic verification of data-centric business processes. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 3–16. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    D’Amorim, M., Roşu, G.: Efficient monitoring of ω-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: TIME, pp. 166–174 (2005)Google Scholar
  11. 11.
    De Giacomo, G., De Masellis, R., Rosati, R.: Verification of conjunctive artifact-centric services. Int. J. Cooperative Inf. Syst. 21(2), 111–140 (2012)CrossRefGoogle Scholar
  12. 12.
    Dong, G., Su, J., Topor, R.: Nonrecursive incremental evaluation of datalog queries. Annals of Mathematics and Artificial Intelligence 14, 187–223 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Fahland, D., Favre, C., Jobstmann, B., Koehler, J., Lohmann, N., Völzer, H., Wolf, K.: Instantaneous soundness checking of industrial business process models. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 278–293. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Kluwer Academic Press (1998)Google Scholar
  16. 16.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  17. 17.
    Gerede, C.E., Su, J.: Specification and verification of artifact behaviors in business process models. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 181–192. Springer, Heidelberg (2007), http://www.springerlink.com/content/c371144007878627 CrossRefGoogle Scholar
  18. 18.
    Hallé, S., Villemaire, R.: Runtime monitoring of message-based workflows with data. In: EDOC, pp. 63–72 (2008)Google Scholar
  19. 19.
    Hariri, B.B., Calvanese, D., De Giacomo, G., De Masellis, R., Felli, P., Montali, M.: Verification of description logic knowledge and action bases. In: ECAI, pp. 103–108 (2012)Google Scholar
  20. 20.
    Havelund, K., Rosu, G.: Foreword - selected papers from the first international workshop on runtime verification held in paris, july 2001 (rv’01). Formal Methods in System Design 24(2), 99–100 (2004)CrossRefzbMATHGoogle Scholar
  21. 21.
    Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 294–309. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  22. 22.
    Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems - safety. Springer (1995)Google Scholar
  24. 24.
    Nigam, A., Caswell, N.S.: Business artifacts: An approach to operational specification. IBM Systems Journal 42(3), 428–445 (2003)CrossRefGoogle Scholar
  25. 25.
    Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)Google Scholar
  26. 26.
    Snodgrass, R.T. (ed.): The TSQL2 Temporal Query Language. Kluwer (1995)Google Scholar
  27. 27.
    Toman, D.: Expiration of historical databases. In: TIME, pp. 128–135 (2001)Google Scholar
  28. 28.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Riccardo De Masellis
    • 1
  • Jianwen Su
    • 2
  1. 1.Sapienza Università di RomaItaly
  2. 2.University of California at Santa BarbaraUnited States

Personalised recommendations