Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics

• Autorzy: Mateo J. A. , Srba J. , Sørensen M. G.

Identyfikatory

DOI

10.3233/FI-2015-1246

• Języki publikacji: EN

Abstrakty

EN

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 first consider the discrete-time semantics (integer delays) and explore the decidability of the soundness 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. We also discuss the soundness problem in the continuous-time semantics (real-number delays) and show that for nets with nonstrict guards (where the reachability question coincides for both semantics) the soundness checking problem does not in general follow the approach for the discrete semantics and different zone-based techniques are needed for introducing its decidability in the bounded case. 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 (www.tapaal.net).

Słowa kluczowe

EN

timed workflow processes; soundness checking; decidability; verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 140, nr 1
• Strony: 89--121
• Opis fizyczny: Bilbiogr. 27 poz., rys., tab.

Twórcy

autor

Mateo J. A.

• Department of Computer Science Aalborg University, Denmark

autor

Srba J.

• Department of Computer Science Aalborg University, Denmark

autor

Sørensen M. G.

• Department of Computer Science Aalborg University, Denmark

Bibliografia

• [1] van der Aalst, W. M. P.: Verification of Workflow Nets, ICATPN’97, 1248, Springer, 1997, ISBN 3-540-63139-9.
• [2] van der Aalst, W. M. P.: The Application of Petri Nets to Workflow Management, Journal of Circuits, Systems, and Computers, 8(1), 1998, 21–66.
• [3] 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), 2011, 333–363.
• [4] Andersen, M., Larsen, H., Srba, J., Sørensen, M., Taankvist, J.: Verification of Liveness Properties on Closed Timed-Arc Petri Nets, MEMICS’12, 7721, Springer-Verlag, 2013.
• [5] Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits, CONCUR’98, 1466, Springer, 1998, ISBN 978-3-540-64896-3.
• [6] Bertolini, C., Liu, Z., Srba, J.: Verification of Timed Healthcare Workflows Using Component Timed-Arc Petri Nets, FHIES’12, 7789, Springer-Verlag, 2013.
• [7] Bolognesi, T., Lucidi, F., Trigila, S.: From Timed Petri Nets to Timed LOTOS, PSTV’90, North-Holland, Amsterdam, 1990.
• [8] Christov, S., Avrunin, G., Clarke, A., Osterweil, L., Henneman, E.: A benchmark for evaluating software engineering techniques for improving medical processes, SEHC’10, ACM, 2010, ISBN 978-1-60558-973-2.
• [9] Cong, J., Liu, B., Zhang, Z.: Scheduling with soft constraints, ICCAD’09, ACM, 2009, ISSN 1092-3152.
• [10] David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K., Møller, M., Srba, J.: TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets, TACAS’12, 7214, Springer-Verlag, 2012.
• [11] D.B. Poulsen, J. v. V.: Concrete Traces for UPPAAL, 3rd Semester Report at Aalborg University, 2010.
• [12] Dickson, L.: Finiteness of the odd perfect and primitive abundant numbers with distinct factors, American Journal of Mathematics, 35, 1913, 413–422.
• [13] Du, Y., Jiang, C.: Towards a Workflow Model of Real-Time Cooperative Systems, ICFEM’03, 2885, Springer, 2003.
• [14] Flender, C., Freytag, T.: Visualizing the Soundness ofWorkflow Nets, AWPN’06, 267, Department Informatics, University of Hamburg, 2006.
• [15] Hanisch, H.: Analysis of Place/Transition Nets with Timed-Arcs and its Application to Batch Process Control, ICATPN’93, 691, Springer, 1993.
• [16] Hoffman, A. J., Kruskal, J. B.: Integral boundary points of convex polyhedra, Linear Inequalities and Related Systems, Princeton Univ. Press, 38, 1956, 22–46.
• [17] Jacobsen, L., Jacobsen, M., Møller, M., Srba, J.: Verification of Timed-Arc Petri Nets, SOFSEM’11, 2011.
• [18] Jacobsen, L., Jacobsen, M., Møller, M. H.: Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants, MEMICS’09, 13, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2009.
• [19] Larsen, K., Wang, Y.: Time-Abstracted Bisimulation: Implicit Specifications and Decidability, Information and Computation, 134(2), 1997, 75–101, ISSN 0890-5401.
• [20] Ling, S., Schmidt, H.: Time Petri nets for workflow modelling and analysis, SMC’00, 4, IEEE, 2000, ISSN 1062-922X.
• [21] Minsky, M.: Computation: Finite and Infinite Machines, Prentice, 1967.
• [22] Pelayo, F., Cuartero, F., Valero, V., Macia, H., Pelayo, M.: Applying Timed-Arc Petri Nets to improve the performance of the MPEG-2 Encoding Algorithm, MMM’04, IEEE, 2004.
• [23] Sieverding, S., Ellen, C., Battram, P.: Sequence Diagram Test Case Specification and Virtual Integration Analysis using Timed-Arc Petri Nets, FESCA’13, 108, 2013.
• [24] Tiplea, F., Macovei, G.: Timed Workflow Nets, SYNASC’05, IEEE Computer Society, 2005, ISBN 0-7695-2453-2.
• [25] Tiplea, F., Macovei, G.: E-timedWorkflow Nets, SYNASC’06, IEEE Computer Society, 2006, ISBN 0-7695-2740-X.
• [26] Tiplea, F., Macovei, G.: Soundness for S- and A-Timed Workflow Nets Is Undecidable, IEEE Trans. On Systems, Man, and Cybernetics, 39(4), 2009, 924–932.
• [27] V.Valero, Cuartero, F., de Frutos-Escrig, D.: On non-decidability of reachability for timed-arc Petri nets, PNPM’99, IEEE, 1999.