Abstract
For improving efficiency and productivity companies are used to work with workflows that allow them to manage the tasks and steps of business processes. Furthermore, modalities have been designed to allow loose specifications by indicating whether activities are necessary or admissible. This paper aims at verifying modal specifications of coloured workflows with data assigned to the tokens and modified by transitions. To this end, executions of coloured workflow nets are modelled using constraint systems, and constraint solving is used to verify modal specifications specifying necessary or admissible behaviours. An implementation supporting the proposed approach and promising experimental results on an issue tracking system 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
Similar content being viewed by others
Notes
- 1.
For confidentiality reasons, the details about this case study are not given.
- 2.
- 3.
References
Cardoso, J., Mendling, J., Neumann, G., Reijers, H.A.: A discourse on complexity of process models. In: Eder, J., Dustdar, S. (eds.) BPM Workshops 2006. LNCS, vol. 4103, pp. 117–128. Springer, Heidelberg (2006)
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.: Three good reasons for using a petri-net-based workflow management system. J. Inf. Process Integr. Enterp. 428, 161–182 (1997)
van der Aalst, W.M.P., Van Hee, K.M., Houben, G.J.: Modelling and analysing workflow using a Petri-net based approach. In: Workshop on Computer-Supported Cooperative Work, Petri nets and Related Formalisms, pp. 31–50, June 1994
Ellis, C.A., Nutt, G.J.: Modeling and enactment of workflow systems. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691. Springer, Heidelberg (1993)
Liu, D., Wang, J., Chan, S.C.F., Sun, J., Zhang, L.: Modeling workflow processes with colored Petri nets. Comput. Ind. 49(3), 267–281 (2002)
Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1989)
Jensen, K.: Coloured Petri nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Central Models and Their Properties. LNCS, pp. 248–299. Springer, Heidelberg (1987)
Larsen, K.G., Thomsen, B.: A modal process logic. In: 3rd Annual Symposium on Logic in Computer Science, LICS 1988, Edinburgh, UK, pp. 203–210. IEEE CSP, July 1988
Bride, H., Kouchnarenko, O., Peureux, F.: Verifying modal workflow specifications using constraint solving. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 171–186. Springer, Heidelberg (2014)
Murata, T.: Petri nets: Properties, analysis and applications. IEEE 77(4), 541–580 (1989)
Presburger, M.: Über die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Sprawozdanie z I Kongresu metematykw slowiaskich, Warszawa, Poland, pp. 92–101 (1929)
Macworth, A.K.: Consistency in networks of relations. J. Artif. Intell. 8(1), 99–118 (1977)
van Hentenryck, P., Dincbas, M.: Domains in logic programming. In: National Conference on Artificial Intelligence, AAAI 1986, pp. 759–765, August 1986
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Englewood Cliffs (1967)
Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Vilkomir, S., Bowen, J.: Formalization of software testing criteria using the Z notation. In: 25th International Conference on Computer Software and Applications, COMPSAC 2001, Chicago, IL, USA, pp. 351–356. IEEE CSP, October 2001
Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal Petri nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency 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. Springer, Heidelberg (1998)
Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMT-based approach to coverability analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 603–619. Springer, Heidelberg (2014)
Bourdeaud’huy, T., Hanafi, S., Yim, P.: Incremental Integer Linear Programming Models for Petri Nets Reachability Problems. Petri Net: Theory and Applications. InTech, Rijeka (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Bride, H., Kouchnarenko, O., Peureux, F. (2016). Constraint Solving for Verifying Modal Specifications of Workflow Nets with Data. In: Mazzara, M., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2015. Lecture Notes in Computer Science(), vol 9609. Springer, Cham. https://doi.org/10.1007/978-3-319-41579-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-41579-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41578-9
Online ISBN: 978-3-319-41579-6
eBook Packages: Computer ScienceComputer Science (R0)