Workflow Soundness Revisited: Checking Correctness in the Presence of Data While Staying Conceptual

  • Natalia Sidorova
  • Christian Stahl
  • Nikola Trčka
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6051)


A conceptual workflow model specifies the control flow of a workflow together with abstract data information. This model is later on refined to be executed on an information system. It is desirable that correctness properties of the conceptual workflow would be transferrable to its refinements. In this paper, we present classical workflow nets extended with data operations as a conceptual workflow model. For these nets we develop a novel technique to verify soundness. This technique allows us to conclude whether at least one or any refinement of a conceptual workflow model is sound.


Model Check Data Element Enterprise Resource Planning System Concrete Data Soundness Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    van der Aalst, W.M.P.: The Application of Petri Nets to Workflow Management. The Journal of Circuits, Systems and Computers 8(1), 21–66 (1998)CrossRefGoogle Scholar
  2. 2.
    van der Aalst, W.M.P., van Dongen, B.F., Günther, C.W., Mans, R.S., Alves de Medeiros, A.K., Rozinat, A., Rubin, V., Song, M., Verbeek, H.M.W., Weijters, A.J.M.M.: ProM 4.0: Comprehensive Support for Real Process Analysis. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 484–494. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Refinement for Symbolic Model Checking. Journ. of the ACM 50(5), 752–794 (2003)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994); A preliminary version appeared in the Proc. of the POPL 1992Google Scholar
  5. 5.
    Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of the 4th ACM SIGACT-SIGPLAN Symp. on Principles of programming languages (POPL 1977), pp. 238–252. ACM Press, New York (1977)CrossRefGoogle Scholar
  6. 6.
    Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD dissertation, Eindhoven University of Technology (July 1996)Google Scholar
  7. 7.
    Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems (TOPLAS) 19(2), 253–291 (1997)CrossRefGoogle Scholar
  8. 8.
    Dehnert, J., Rittgen, P.: Relaxed soundness of business processes. In: Dittrich, K.R., Geppert, A., Norrie, M.C. (eds.) CAiSE 2001. LNCS, vol. 2068, pp. 157–170. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Dumas, M., van der Aalst, W.M.P., ter Hofstede, A.H.M.: Process-Aware Information Systems: Bridging People and Software through Process Technology. Wiley & Sons, Chichester (2005)CrossRefGoogle Scholar
  10. 10.
    Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  11. 11.
    Heinze, T.S., Amme, W., Moser, S.: Generic CSSA-based pattern over boolean data for an improved WS-BPEL to petri net mappping. In: Mellouk, A., Bi, J., Ortiz, G., Chiu, D.K.W., Popescu, M. (eds.) Third International Conference on Internet and Web Applications and Services, ICIW 2008, Athens, Greece, June 8-13, pp. 590–595. IEEE Computer Society, Los Alamitos (2008)CrossRefGoogle Scholar
  12. 12.
    Heinze, T.S., Amme, W., Moser, S.: A restructuring method for WS-BPEL business processes based on extended workflow graphs. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 211–228. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. 13.
    Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental Verification by Abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. 14.
    Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)Google Scholar
  15. 15.
    Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design 6(1), 11–44 (1995)zbMATHCrossRefGoogle Scholar
  16. 16.
    Moser, S., Martens, A., Görlach, K., Amme, W., Godlinski, A.: Advanced verification of distributed WS-BPEL business processes incorporating CSSA-based data flow analysis. In: 2007 IEEE International Conference on Services Computing (SCC 2007), Salt Lake City, Utah, USA, July 9-13, pp. 98–105. IEEE Computer Society, Los Alamitos (2007)CrossRefGoogle Scholar
  17. 17.
    Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for ctl. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)Google Scholar
  18. 18.
    Trčka, N.: Workflow Soundness and Data Abstraction: Some negative results and some open issues. In: Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC), pp. 19–25 (2009)Google Scholar
  19. 19.
    Trčka, N., van der Aalst, W.M.P., Sidorova, N.: Data-Flow Anti-Patterns: Discovering Data-Flow Errors in Workflows. In: van Eck, P., Gordijn, J., Wieringa, R. (eds.) CAiSE 2009. LNCS, vol. 5565, pp. 425–439. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Natalia Sidorova
    • 1
  • Christian Stahl
    • 1
  • Nikola Trčka
    • 1
  1. 1.Department of Mathematics and Computer ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations