Skip to main content
SpringerLink
Log in

Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes

  • Conference paper
FM 2015: Formal Methods (FM 2015)

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

Included in the following conference series:

Abstract

We study modularity, run-time adaptation and refinement under safety and liveness constraints in event-based process models with dynamic sub-process instantiation. The study is part of a larger programme to provide semantically well-founded technologies for modelling, implementation and verification of flexible, run-time adaptable processaware information systems, moved into practice via the Dynamic Condition Response (DCR) Graphs notation co-developed with our industrial partner. Our key contributions are: (1) A formal theory of dynamic subprocess instantiation for declarative, event-based processes under safety and liveness constraints, given as the DCR* process language, equipped with a compositional operational semantics and conservatively extending the DCR Graphs notation; (2) an expressiveness analysis revealing that the DCR* process language is Turing-complete, while the fragment corresponding to DCR Graphs (without dynamic sub-process instantiation) characterises exactly the languages that are the union of a regular and an omega-regular language; (3) a formalisation of run-time refinement and adaptation by composition for DCR* processes and a proof that such refinement is undecidable in general; and finally (4) a decidable and practically useful sub-class of run-time refinements. Our results are illustrated by a running example inspired by a recent Electronic Case Management solution based on DCR Graphs and delivered by our industrial partner. An online prototype implementation of the DCR* language (including examples from the paper) and its visualisation as DCR Graphs can be found at http://tiger.itu.dk:8020/.

Supported by the Velux foundation (grant 33295) and Innovation Fund Denmark.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. van der Aalst, W.M.P.: The application of petri nets to workflow management. Journal of Circuits, Systems, and Computers 8(1), 21–66 (1998)

    Article  Google Scholar 

  2. van der Aalst, W.M.P., ter Hofstede, A.H.M., Weske, M.: Business process management: A survey. In: van der Aalst, W.M.P., ter Hofstede, A.H.M., Weske, M. (eds.) BPM 2003. LNCS, vol. 2678, pp. 1–12. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. van der Aalst, W.M.P., Pesic, M.: DecSerFlow: Towards a truly declarative service flow language. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 1–23. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. van der Aalst, W.M.P., Pesic, M., Schonenberg, H., Westergaard, M., Maggi, F.M.: Declare. Webpage (2010), http://www.win.tue.nl/declare/

  5. Anderson, G., Rathke, J.: Dynamic software update for message passing programs. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 207–222. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Baldan, P., Corradini, A., Montanari, U.: Contextual petri nets, asymmetric event structures, and processes. Information and Computation 171, 1–49 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  7. Barthe, G., Pardo, A., Schneider, G. (eds.): SEFM 2011. LNCS, vol. 7041. Springer, Heidelberg (2011)

    MATH  Google Scholar 

  8. Bravetti, M., Giusto, C.D., Pérez, J.A., Zavattaro, G.: Steps on the road to component evolvability. In: Proceedings of the 7th International Conference on Formal Aspects of Component Software, FACS 2010, pp. 295–299 (2012), http://dx.doi.org/10.1007/978-3-642-27269-1_19

  9. Bravetti, M., Giusto, C.D., Pérez, J.A., Zavattaro, G.: Adaptable processes. Logical Methods in Computer Science 8(4) (2012)

    Google Scholar 

  10. Debois, S., Hildebrandt, T., Marquard, M., Slaats, T.: A case for declarative process modelling: Agile development of a grant application system. In: EDOCW/AdaptiveCM 2014, pp. 126 – 133. IEEE (September 2014)

    Google Scholar 

  11. Debois, S., Hildebrandt, T., Slaats, T.: Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes (full version) (2015), http://www.itu.dk/~debois/dcrstar-tr.pdf

  12. Debois, S., Hildebrandt, T.T., Slaats, T.: Hierarchical declarative modelling with refinement and sub-processes. In: Sadiq, S., Soffer, P., Völzer, H. (eds.) BPM 2014. LNCS, vol. 8659, pp. 18–33. Springer, Heidelberg (2014), http://dx.doi.org/10.1007/978-3-319-10172-9

    Chapter  Google Scholar 

  13. Debois, S., Hildebrandt, T.T., Slaats, T., Yoshida, N.: Type checking liveness for collaborative processes with bounded and unbounded recursion. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 1–16. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  14. Esparza, J., Melzer, S.: Model checking LTL using constraint programming. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 1–20. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  15. Fecher, H., Majster-Cederbaum, M.: Event structures for arbitrary disruption. Fundam. Inf. 68(1-2), 103–130 (2005)

    MATH  MathSciNet  Google Scholar 

  16. van Glabbeek, R.J., Vaandrager, F.W.: Bundle event structures and CCSP. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 57–71. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Hildebrandt, T.T., Mukkamala, R.R.: Declarative event-based workflow as distributed dynamic condition response graphs. In: PLACES. EPTCS. EPTCS, vol. 69, pp. 59–73 (2010)

    Google Scholar 

  18. Hildebrandt, T.T., Mukkamala, R.R., Slaats, T.: Nested dynamic condition response graphs. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 343–350. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Hildebrandt, T.T., Mukkamala, R.R., Slaats, T., Zanitti, F.: Contracts for cross-organizational workflows as timed dynamic condition response graphs. J. Log. Algebr. Program. 82(5-7), 164–185 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  20. Hoogers, P.W., Kleijn, H.C.M., Thiagarajan, P.S.: An event structure semantics for general petri nets. Theoretical Computer Science 153(1-2), 129–170 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  21. Janneck, J.W., Esser, R.: Higher-order petri net modelling: Techniques and applications. In: Proceedings of the Conference on Application and Theory of Petri Nets: Formal Methods in Software Engineering and Defence Systems, CRPIT 2002, pp. 17–25 (2002)

    Google Scholar 

  22. Katoen, J.P.: Quantitative and qualitative extensions of event structures. Ph.D. thesis, University of Twente, Enschede (April 1996)

    Google Scholar 

  23. Langerak, R.: Transformations and Semantics for LOTOS. Universiteit Twente (1992)

    Google Scholar 

  24. Langerak, R., Brinksma, E., Katoen, J.-P.: Causal ambiguity and partial orders in event structures. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 317–331. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  25. Latvala, T., Mäkelä, M.: LTL model checking for modular petri nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 298–311. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  26. Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall (1967)

    Google Scholar 

  27. Montali, M.: Specification and Verification of Declarative Open Interaction Models - A Logic-Based Approach, LNBIP, vol. 56. Springer, Heidelberg (2010)

    Google Scholar 

  28. Mukkamala, R.R.: A Formal Model For Declarative Workflows: Dynamic Condition Response Graphs. Ph.D. thesis, IT University of Copenhagen (June 2012)

    Google Scholar 

  29. Mukkamala, R.R., Hildebrandt, T., Slaats, T.: Towards trustworthy adaptive case management with dynamic condition response graphs. In: EDOC, pp. 127–136. IEEE (2013)

    Google Scholar 

  30. Object Management Group BPMN Technical Committee: Business Process Model and Notation, version 2.0, http://www.omg.org/spec/BPMN/2.0/PDF

  31. Pinna, G., Poign, A.: On the nature of events: another perspective in concurrency. Theoretical Computer Science 138(2), 425–454 (1995), meeting on the mathematical foundation of programing semantics

    Google Scholar 

  32. Reichert, M., Weber, B.: Enabling Flexibility in Process-Aware Information Systems - Challenges, Methods, Technologies. Springer (2012)

    Google Scholar 

  33. Russell, N., ter Hofstede, A., van der Aalst, W., Mulyar, N.: Workflow control-flow patterns: A revised view (2006), http://BPMcenter.org

  34. Sibertin-Blanc, C., Mauran, P., Padiou, G.: Safe Adaptation of Component Coordination. In: Proceedings of the Third International Workshop on Coordination and Adaption Techniques for Software Entities, vol. 189, pp. 69–85 (juillet 2007)

    Google Scholar 

  35. Slaats, T., Mukkamala, R.R., Hildebrandt, T., Marquard, M.: Exformatics declarative case management workflows as DCR graphs. In: Daniel, F., Wang, J., Weber, B. (eds.) BPM 2013. LNCS, vol. 8094, pp. 339–354. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  36. Winskel, G.: Events in Computation. Ph.D. thesis, University of Edinburgh (1980)

    Google Scholar 

  37. Zugal, S., Soffer, P., Pinggera, J., Weber, B.: Expressiveness and understandability considerations of hierarchy in declarative business process models. In: Bider, I., et al. (eds.) EMMSAD 2012 and BPMDS 2012. LNBIP, vol. 113, pp. 167–181. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IT University of Copenhagen, København S, Denmark

    Søren Debois, Thomas Hildebrandt & Tijs Slaats

  2. Exformatics A/S, København S, Denmark

    Tijs Slaats

Authors
  1. Søren Debois
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Hildebrandt
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tijs Slaats
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Søren Debois .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Nikolaj Bjørner

  2. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands

    Frank de Boer

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Debois, S., Hildebrandt, T., Slaats, T. (2015). Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19249-9_10

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19248-2

  • Online ISBN: 978-3-319-19249-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation