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

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9109
• 期：1
• 页码：143-160
• 全文大小：330 KB
• 参考文献：1.van der Aalst, W.M.P.: The application of petri nets to workflow management. Journal of Circuits, Systems, and Computers聽8(1), 21鈥?6 (1998)View Article
  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鈥?2. Springer, Heidelberg (2003)View Article
  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鈥?3. Springer, Heidelberg (2006)View Article
  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鈥?22. Springer, Heidelberg (2012)View Article
  6.Baldan, P., Corradini, A., Montanari, U.: Contextual petri nets, asymmetric event structures, and processes. Information and Computation聽171, 1鈥?9 (2001)View Article MATH MathSciNet
  7.Barthe, G., Pardo, A., Schneider, G. (eds.): SEFM 2011. LNCS, vol.聽7041. Springer, Heidelberg (2011)MATH
  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鈥?99 (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)
  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)
  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鈥?3. Springer, Heidelberg (2014), http://dx.doi.org/10.1007/978-3-319-10172-9 View Article
  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鈥?6. Springer, Heidelberg (2014)View Article
  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鈥?0. Springer, Heidelberg (1997)View Article
  15.Fecher, H., Majster-Cederbaum, M.: Event structures for arbitrary disruption. Fundam. Inf.聽68(1-2), 103鈥?30 (2005)MATH MathSciNet
  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鈥?1. Springer, Heidelberg (2003)View Article
  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鈥?3 (2010)
  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鈥?50. Springer, Heidelberg (2012)View Article
  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鈥?85 (2013)View Article MATH MathSciNet
  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鈥?70 (1996)View Article MATH MathSciNet
  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鈥?5 (2002)
  22.Katoen, J.P.: Quantitative and qualitative extensions of event structures. Ph.D. thesis, University of Twente, Enschede (April 1996)
  23.Langerak, R.: Transformations and Semantics for LOTOS. Universiteit Twente (1992)
  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鈥?31. Springer, Heidelberg (1997)View Article
  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鈥?11. Springer, Heidelberg (2004)View Article
  26.Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall (1967)
  27.Montali, M.: Specification and Verification of Declarative Open Interaction Models - A Logic-Based Approach, LNBIP, vol.聽56. Springer, Heidelberg (2010)
  28.Mukkamala, R.R.: A Formal Model For Declarative Workflows: Dynamic Condition Response Graphs. Ph.D. thesis, IT University of Copenhagen (June 2012)
  29.Mukkamala, R.R., Hildebrandt, T., Slaats, T.: Towards trustworthy adaptive case management with dynamic condition response graphs. In: EDOC, pp. 127鈥?36. IEEE (2013)
  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鈥?54 (1995), meeting on the mathematical foundation of programing semantics
  32.Reichert, M., Weber, B.: Enabling Flexibility in Process-Aware Information Systems - Challenges, Methods, Technologies. Springer (2012)
  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鈥?5 (juillet 2007)
  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鈥?54. Springer, Heidelberg (2013)View Article
  36.Winskel, G.: Events in Computation. Ph.D. thesis, University of Edinburgh (1980)
  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鈥?81. Springer, Heidelberg (2012)View Article
  
• 作者单位：S酶ren Debois (15)
  Thomas Hildebrandt (15)
  Tijs Slaats (15) (16)
  
  15. IT University of Copenhagen, K酶benhavn S, Denmark
  16. Exformatics A/S, K酶benhavn S, Denmark
  
• 丛书名：FM 2015: Formal Methods
• ISBN：978-3-319-19249-9
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

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