Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Assessing SMT and CLP approaches for workflow nets verification

  • FMICS-AVoCS
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

In the actual business world, companies rely more and more on workflows to model the core of their business processes. In this context, the focus of workflow analysts is made on the verification of workflows specifications, in particular of modal specifications that allow the description of necessary or admissible behaviors. The design and the analysis of business processes commonly relies on workflow nets, a suited class of Petri nets. The goal of this paper is to evaluate and compare in a deep way two resolution methods—satisfiability modulo theory and constraint logic programming—applied to the verification of modal specifications over workflow nets. Firstly, it provides a concise description of the verification methods based on constraint solving. Secondly, it introduces the toolchain developed to automate the full verification process. Thirdly, it describes the experimental protocol designed to evaluate and compare the scalability and efficiency of both resolution approaches and reports on the obtained results. Finally, these obtained results are discussed in detail, lessons learned from these experiments are given, and, on the basis of experiments feedback, directions for improvement and future work are suggested.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18
Fig. 19
Fig. 20

Similar content being viewed by others

Notes

  1. www.smtcomp.org.

  2. www.minizinc.org/challenge.html.

References

  1. Bellegarde, F., Darlot, C., Julliand, J., Kouchnarenko, O.: Reformulation: a way to combine dynamic properties and b refinement. In: FME, vol. 2021, pp. 2–19. Springer, Berlin (2001)

  2. Bi, H.H., Zhao, J.L.: Applying propositional logic to workflow verification. Inf. Technol. Manag. 5(3–4), 293–318 (2004)

    Article  Google Scholar 

  3. Bride, H., Kouchnarenko, O., Peureux, F.: Verifying modal workflow specifications using constraint solving. In: Proceedings of the International Conference on Integrated Formal Methods (IFM’14), Volume 8739 of LNCS, pp. 171–186, Bertinoro, Italy, September 2014. Springer

  4. Bride, H., Kouchnarenko, O., Peureux, F.: Constraint solving for verifying modal specifications of workflow nets with data. In: Proceedings of 10th International Ershov Informatics Conference on Perspectives of System Informatics (PSI’15), Volume 9609 of LNCS, pp. 75–90, Kazan, Russia, August 2015. Springer

  5. Bride, H., Kouchnarenko, O., Peureux, F.: Reduction of workflow nets for generalised soundness verification. In: Proceedings of the 18th International Conference on Verification, Model-Checking, and Abstract Interpretation (VMCAI’17), Volume 10145 of LNCS, pp. 91–111, Paris, France, January 2017. Springer

  6. Bride, H., Kouchnarenko, O., Peureux, F., Voiron, G.: Comparaison des approches SMT et CSP appliquées à la vérification de réseaux workflows. In: Actes des 15èmes journées sur les Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL’16), pp. 11–12, Besançon, France, June 2016

  7. Bride, H., Kouchnarenko, O., Peureux, F., Voiron, G.: Workflow nets verification: SMT or CLP? In: Proceedings of the 21st International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS-AVoCS’16), Volume 9933 of LNCS, pp. 1–17, Pisa, Italy, September 2016. Springer

  8. Carlsson, M., et al.: SICStus Prolog User’s Manual (Release 4.2.3). Swedish Institute of Computer Science, Kista (2012)

    Google Scholar 

  9. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  10. De Moura, L., Bjørner, N.: Z3: an efficient smt solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340. Springer (2008)

  11. De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

    Article  Google Scholar 

  12. Edward, P.K.T.: Foundations of Constraint Satisfaction. Computation in Cognitive Science. Academic Press, Cambridge (1993)

    Google Scholar 

  13. Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal petri nets. Trans. Petri Nets Other Models Concurr. 5, 96–120 (2012)

    Article  MATH  Google Scholar 

  14. Espada, M.V., van de Pol, J.: Accelerated modal abstractions of labelled transition systems. In: International Conference on Algebraic Methodology and Software Technology, pp. 338–352. Springer (2006)

  15. Fahland, D., Favre, C., Koehler, J., Lohmann, N., Völzer, H., Wolf, K.: Analysis on demand: instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70(5), 448–466 (2011)

    Article  Google Scholar 

  16. Goedertier, S., Vanthienen, J.: Designing compliant business processes with obligations and permissions. In: Business Process Management Workshops, pp. 5–14. Springer (2006)

  17. Governatori, G., Milosevic, Z., Sadiq, S.: Compliance checking between business processes and business contracts. In: EDOC’06: Proceedings of the 10th IEEE International Enterprise Distributed Object Computing Conference 2006, pp. 221–232. IEEE (2006)

  18. Haddad, S.: Decidability and complexity of Petri net problems. In: Petri Nets: Fundamental Models, Verification and Applications, pp. 87–122 (2009). https://doi.org/10.1002/9780470611647.ch4

  19. Kleine, M., Göthel, T.: Specification, verification and implementation of business processes using CSP. In: TASE, pp. 145–154. IEEE Computer Society (2010)

  20. Kordon, F., Garavel, H., Hillah, L. M., Hulin-Hubard, F., Berthomieu, B., Ciardo, G., Colange, M., Dal Zilio, S., Amparore, E., Beccuti, M., Liebke, T., Meijer, J., Miner, A., Rohr, C., Srba, J., Thierry-Mieg, Y., van de Pol, J., Wolf, K.: Complete Results for the 2017 Edition of the Model Checking Contest. http://mcc.lip6.fr/2017/results.php (2017). Accessed Jan 2018

  21. Kouchnarenko, O., Sidorova, N., Trcka, N.: Petri nets with may/must semantics. In: Workshop on Concurrency, Specification, and Programming - CS&P 2009, vol. 1, Kraków-Przegorzaly, Poland, September 2009

  22. Larsen, K.G.: Modal specifications. In: Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, pp. 232–246, London, UK. Springer (1990)

  23. Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science, 1988. LICS ’88, pp. 203–210 (1988)

  24. Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  25. Monakova, G., Kopp, O., Leymann, F., Moser, S., Schäfers, K.: Verifying business rules using an SMT solver for BPEL processes. In: BPSC, Volume 147 of LNI, pp. 81–94. GI (2009)

  26. Murata, T.: Petri nets: properties, analysis and applications. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  27. Petri, C.A.: Kommunikation mit Automaten. PhD thesis, Universität Hamburg (1962)

  28. Pólrola, A., Cybula, P., Meski, A.: Smt-based reachability checking for bounded time Petri nets. Fundam. Inform. 135(4), 467–482 (2014)

    MathSciNet  MATH  Google Scholar 

  29. Salimifard, K., Wright, M.: Petri net-based modelling of workflow systems: an overview. Eur. J. Oper. Res. 134(3), 664–676 (2001)

    Article  MATH  Google Scholar 

  30. Schmidt, K.: Lola a low level analyser. In: International Conference on Application and Theory of Petri Nets, pp. 465–474. Springer (2000)

  31. Soliman, S.: Finding minimal p/t-invariants as a csp. In: Proceedings of the 4th Workshop on Constraint Based Methods for Bioinformatics WCB, vol. 8 (2008)

  32. Suzuki, I., Murata, T.: A method for stepwise refinement and abstraction of Petri nets. J. Comput. Syst. Sci. 27(1), 51–76 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  33. Van Der Aalst, W.M.P.: Three good reasons for using a Petri-net-based workflow management system. In: Proceedings of the International Working Conference on Information and Process Integration in Enterprises (IPIC’96), pp. 179–201. Cambridge (1996)

  34. van der Aalst, W.M.P.: Verification of workflow nets. In: Proceedinga of the 18th International Conference on Application and Theory of Petri Nets, ICATPN ’97, pp. 407–426, London, UK. Springer (1997)

  35. van der Aalst, W.M.P.: The application of Petri nets to workflow management. J. Circuits Syst. Comput. 08(01), 21–66 (1998)

    Article  Google Scholar 

  36. Van Der Aalst, W.M.P.: Woflan: a Petri-net-based workflow analyzer. Syst. Anal. Model. Simul. 35(3), 345–358 (1999)

    MATH  Google Scholar 

  37. van der Aalst, W.M.P., van Hee, K.M., ter Hofstede, A.H.M., Sidorova, N., Verbeek, H.M.W., Voorhoeve, M., Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis. Form. Asp. Comput. 23(3), 333–363 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  38. Van Hee, K., Sidorova, N., Voorhoeve, M.: Soundness and separability of workflow nets in the stepwise refinement approach. In ICATPN, vol. 2679, pp. 337–356. Springer (2003)

  39. Van Hee, K.M., Liu, Z.: Generating benchmarks by random stepwise refinement of Petri nets. In: ACSD/Petri Nets Workshops, pp. 403–417 (2010)

  40. Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Log. Methods Comput. Sci. 8(3), 1–15 (2012)

    MathSciNet  MATH  Google Scholar 

  41. Wong, P.Y.H., Gibbons, J.: A process-algebraic approach to workflow specification and refinement. In Proceedings of the 6th International Conference on Software Composition, SC’07, pp. 51–65. Springer, Berlin (2007)

Download references

Author information

Authors and Affiliations

  1. Institut FEMTO-ST – UMR CNRS 6174, Univ. Bourgogne Franche-Comté, 16, route de Gray, 25030, Besançon, France

    Hadrien Bride, Olga Kouchnarenko, Fabien Peureux & Guillaume Voiron

  2. LS2N, UMR CNRS 6004, Ecole Centrale de Nantes, 1 Rue de la No, 44300, Nantes, France

    Hadrien Bride

Authors
  1. Hadrien Bride
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olga Kouchnarenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fabien Peureux
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Guillaume Voiron
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fabien Peureux.

A Appendix: Verifying modal specification using model checking

A Appendix: Verifying modal specification using model checking

In this appendix we describe the methodology used to verify modal specifications using a CTL Petri net model checker such as LoLa [30].

As stated in Sect. 2 modal specifications are a proper subset of CTL, it is therefore possible to check any modal specifications of a given workflow net using any CTL Petri net model checker. To this end, the considered workflow net needs to be transformed into an equivalent Petri net such that the validity of any modal specifications is equivalent to the validity of the corresponding CTL formulae. The aim of this transformation is to introduce for each transition t a new place \(p_t\) which is marked if and only if t has been fired at least once during an execution marking the final place o.

To produce a Petri net \(\tilde{N}\) from a workflow net \(N = \langle P,T,F \rangle \) the transformation proceeds as follows. For each transition \(t \in T\) the transformation introduces two new places, respectively, denoted \(f_t\) and \(p_t\). Further, the transformation then replaces each transition t by two transitions, respectively, denoted \(t_f\) and \(t_e\) such that:

  • \(^{\bullet }t_f = ^{\bullet }t \cup \{f_t\}\)

  • \(t_f^{\bullet } = t^{\bullet } \cup \{p_t\}\)

  • \(^{\bullet }t_e = ^{\bullet }t \cup \{p_t\}\)

  • \(t_e^{\bullet } = t^{\bullet } \cup \{p_t\}\)

Note that if the state space of N is finite, then the state space of \(\tilde{N}\) is finite too.

The initial marking of \(\tilde{N}\) is the marking assigning a single token to place i and places \(f_t\) where \(t \in T\) (and none to other places).

By construction, for any execution \(\sigma \) of N, there exist a corresponding execution \(\tilde{\sigma }\) of \(\tilde{N}\) obtained by replacing, for every transition \(t \in T\), the first occurrence of t by \(t_f\) and the following occurrences of t by \(t_e\). Conversely, for any execution \(\tilde{\sigma }\) of \(\tilde{N}\) there exists a corresponding execution \(\sigma \) of N obtained by replacing, for every transition \(t \in T\), all occurrences of \(t_f\) and \(t_e\) by t.

Further, given a modal formula \(f \in S\) of the workflow net N, we define CTL(f) as the formula obtained after replacing, for every transition \(t \in T\), the corresponding terminal symbols of the modal formula f by \(p_t=1\).

Consequently, as for each transition t the new place \(p_t\) is marked if and only if t has been fired at least once during an execution, we have:

  • \(N \models _{may} f \Leftrightarrow \tilde{N} \models EF (o=1) \Rightarrow (CTL(f))\)

  • \(N \models _{must} f \Leftrightarrow \tilde{N} \models AF (o=1) \Rightarrow (CTL(f))\)

This enables the verification of modal specifications described in this paper using CTL model checker, and consequently this link makes it possible to compare verification approaches by constraint solving and by model checking.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bride, H., Kouchnarenko, O., Peureux, F. et al. Assessing SMT and CLP approaches for workflow nets verification. Int J Softw Tools Technol Transfer 20, 467–491 (2018). https://doi.org/10.1007/s10009-018-0486-5

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-018-0486-5

Keywords

Search

Navigation