Advertisement

Soundness of Timed-Arc Workflow Nets

  • José Antonio Mateo
  • Jiří Srba
  • Mathias Grund Sørensen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8489)

Abstract

Analysis of workflow processes with quantitative aspects like timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and study the foundational problems of soundness and strong (time-bounded) soundness. We explore the decidability of these problems and show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable. For general timed-arc workflow nets soundness and strong soundness become undecidable, though we can design efficient verification algorithms for the subclass of bounded nets. Finally, we demonstrate the usability of our theory on the case studies of a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow. The implementation of the algorithms is freely available as a part of the model checker TAPAAL.

Keywords

Input Place Output Place Error Trace Minimum Execution Time Urgent Transition 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Andersen, M., Gatten Larsen, H., Srba, J., Grund Sørensen, M., Haahr Taankvist, J.: Verification of liveness properties on closed timed-arc Petri nets. In: Kučera, A., Henzinger, T.A., Nešetřil, J., Vojnar, T., Antoš, D. (eds.) MEMICS 2012. LNCS, vol. 7721, pp. 69–81. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  2. 2.
    Bertolini, C., Liu, Z., Srba, J.: Verification of timed healthcare workflows using component timed-arc Petri nets. In: Weber, J., Perseil, I. (eds.) FHIES 2012. LNCS, vol. 7789, pp. 19–36. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    Bolognesi, T., Lucidi, F., Trigila, S.: From timed Petri nets to timed LOTOS. In: PSTV 1990, pp. 1–14. North-Holland, Amsterdam (1990)Google Scholar
  4. 4.
    Christov, S.C., Avrunin, G.S., Clarke, A.L., Osterweil, L.J., Henneman, E.A.: A benchmark for evaluating software engineering techniques for improving medical processes. In: SEHC 2010, pp. 50–56. ACM (2010)Google Scholar
  5. 5.
    David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: Integrated development environment for timed-arc Petri nets. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  6. 6.
    Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with distinct factors. American Journal of Mathematics 35, 413–422 (1913)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Du, Y., Jiang, C.: Towards a workflow model of real-time cooperative systems. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 452–470. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Flender, C., Freytag, T.: Visualizing the soundness of workflow nets. In: AWPN 2006, Department Informatics, University of Hamburg, vol. 267 (2006)Google Scholar
  9. 9.
    Hanisch, H.M.: Analysis of place/transition nets with timed-arcs and its application to batch process control. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 282–299. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  10. 10.
    Ling, S., Schmidt, H.: Time Petri nets for workflow modelling and analysis. In: SMC 2000, vol. 4, pp. 3039–3044. IEEE (2000)Google Scholar
  11. 11.
    Pelayo, F.L., Cuartero, F., Valero, V., Macia, H., Pelayo, M.L.: Applying timed-arc Petri nets to improve the performance of the MPEG-2 encoding algorithm. In: MMM 2004, pp. 49–56. IEEE (2004)Google Scholar
  12. 12.
    Sieverding, S., Ellen, C., Battram, P.: Sequence diagram test case specification and virtual integration analysis using timed-arc Petri nets. In: FESCA 2013. EPTCS, vol. 108, pp. 17–31 (2013)CrossRefGoogle Scholar
  13. 13.
    Tiplea, F.L., Macovei, G.: Timed workflow nets. In: SYNASC 2005, pp. 361–366. IEEE Computer Society (2005)Google Scholar
  14. 14.
    Tiplea, F.L., Macovei, G.: E-timed workflow nets. In: SYNASC 2006, pp. 423–429. IEEE Computer Society (2006)Google Scholar
  15. 15.
    Tiplea, F.L., Macovei, G.: Soundness for s- and a-timed workflow nets is undecidable. IEEE Trans. on Systems, Man, and Cybernetics 39(4), 924–932 (2009)CrossRefGoogle Scholar
  16. 16.
    van der Aalst, W.M.P.: Verification of workflow nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 407–426. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    van der Aalst, W.M.P., van Hee, K., ter Hofstede, A.H.M., Sidorova, N., Verbeek, H.M.W., Voorhoeve, M., Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis. Formal Aspects of Comp. 23(3), 333–363 (2011)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Valero, V., Cuartero, F., de Frutos-Escrig, D.: On non-decidability of reachability for timed-arc Petri nets. In: PNPM 1999, pp. 188–196. IEEE (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • José Antonio Mateo
    • 1
    • 2
  • Jiří Srba
    • 1
  • Mathias Grund Sørensen
    • 1
  1. 1.Department of Computer ScienceAalborg UniversityAalborg EastDenmark
  2. 2.Department of Computer ScienceUniversity of Castilla-La ManchaAlbaceteSpain

Personalised recommendations