Abstract
Nowadays workflows are extensively used by companies to improve organizational efficiency and productivity. This paper focuses on the verification of modal workflow specifications using constraint solving as a computational tool. Its main contribution consists in developing an innovative formal framework based on constraint systems to model executions of workflow Petri nets and their structural properties, as well as to verify their modal specifications. Finally, an implementation and promising experimental results constitute a practical contribution.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
van der Aalst, W.M.P., ter Hofstede, A.H.M.: YAWL: Yet another workflow language. Journal of Information Systems 30(4), 245–275 (2005)
Dumas, M., ter Hofstede, A.H.M.: UML activity diagrams as a workflow specification language. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 76–90. Springer, Heidelberg (2001)
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)
van der Aalst, W.M.P.: Three good reasons for using a Petri-net-based workflow management system. Journal of Information and Process Integration in Enterprises 428, 161–182 (1997)
Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)
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)
Heiner, M., Gilbert, D., Donaldson, R.: Petri nets for systems and synthetic biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008)
Macworth, A.K.: Consistency in networks of relations. Journal of Artificial Intelligence 8(1), 99–118 (1977)
Tsang, E.: Foundation of constraint satisfaction. Academic Press (1993)
van Hee, K., et al.: Yasper: a tool for workflow modeling and analysis. In: Proc. of the 6th Int. Conf. on Application of Concurrency to System Design (ACSD 2006), Turku, Finland, pp. 279–282. IEEE CS (June 2006)
Bonet, P., Lladó, C.M., Puijaner, R., Knottenbelt, W.J.: PIPE v2.5: A Petri net tool for performance modelling. In: Proc. of the 23rd Latin American Conference on Informatics (CLEI 2007), San Jose, Costa Rica (October 2007)
Carlsson, M., et al.: SICStus Prolog user’s manual (Release 4.2.3). Swedish Institute of Computer Science, Kista, Sweden (October 2012)
Kouchnarenko, O., Sidorova, N., Trcka, N.: Petri nets with may/must semantics. In: Proc. of the Workshop on Concurrency, Specification, and Programming (CS&P 2009), Kraków-Przegorzaly, Poland, pp. 291–302 (September 2009)
van der Aalst, W.M.P.: Business process management demystified: A tutorial on models, systems and standards for workflow management. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 1–65. Springer, Heidelberg (2004)
Larsen, K.G., Thomsen, B.: A modal process logic. In: Proc. of the 3rd Annual Symp. on Logic in Computer Science (LICS 1988), pp. 203–210. IEEE (July 1988)
Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal petri nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 96–120. Springer, Heidelberg (2012)
Desel, J.: Basic linear algebraic techniques for place/transition nets. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 257–308. Springer, Heidelberg (1998)
Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 224–238. Springer, Heidelberg (2011)
Schmidt, K.: Narrowing Petri net state spaces using the state equation. Fundamenta Informaticae 47(3-4), 325–335 (2001)
Soliman, S.: Finding minimal P/T-invariants as a CSP. In: Proc. of the 4th Workshop on Constraint Based Methods for Bioinformatics (WCB 2008) (May 2008)
Melzer, S., Esparza, J.: Checking system properties via integer programming. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol. 1058, pp. 250–264. Springer, Heidelberg (1996)
Bourdeaud’huy, T., Hanafi, S., Yim, P.: Incremental integer linear programming models for Petri nets reachability problems. Petri Net: Theory and Applications, pp. 401–434 (February 2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bride, H., Kouchnarenko, O., Peureux, F. (2014). Verifying Modal Workflow Specifications Using Constraint Solving. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_11
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)