Can I Execute My Scenario in Your Net? VipTool Tells You! | SpringerLink
Skip to main content
Springer Nature Link
Log in

Can I Execute My Scenario in Your Net? VipTool Tells You!

  • Conference paper
Petri Nets and Other Models of Concurrency - ICATPN 2006 (ICATPN 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4024))

Included in the following conference series:

  • 667 Accesses

Abstract

This paper describes the verification module (the VipVerify Module) of the VipTool [4]. VipVerify allows to verify whether a given scenario is an execution of a system model, given by a Petri net. Scenarios can be graphically specified by means of Labeled Partial Orders (LPOs). A specified LPO is an execution of a Petri net if it is a (partial) sequentialization of an LPO generated by a process of the net. We have shown in [2] that the executability of an LPO can be tested by a polynomial algorithm. The VipVerify Module implements this algorithm. If the test is positive, the corresponding process is computed and visualized. If the test is negative, a maximal executable prefix of the LPO is computed and visualized, together with a corresponding process and the set of those following events in the LPO which are not enabled to occur after the occurrence of the prefix. Further, the VipVerify Module allows to test in polynomial time whether a scenario equals an execution with minimal causality. A small case study illustrates the verification of scenarios w.r.t. business process models.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Lorenz, R., Juhás, G.: Towards Synthesis of Petri nets from Scenarios. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 302–321. Springer, Heidelberg (2006) (accepted)

    Chapter  Google Scholar 

  2. Juhás, G., Lorenz, R., Desel, J.: Can I Execute my Scenario in your Net? In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 289–308. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Desel, J., Juhás, G., Lorenz, R., Neumair, C.: Modeling and Validation with VipTool. In: van der Aalst, W.M.P., ter Hofstede, A.H.M., Weske, M. (eds.) BPM 2003. LNCS, vol. 2678, pp. 380–389. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. VipTool-Homepage, http://www.informatik.ku-eichstaett.de/projekte/vip/

  5. van der Aalst, W.M.P., Desel, J., Oberweis, A. (eds.): Business Process Management. LNCS, vol. 1806. Springer, Heidelberg (2000)

    Google Scholar 

  6. Desel, J.: Validation of Process Models by Construction of Process Nets. In: [5], pp. 110–128

    Google Scholar 

  7. Desel, J.: Model Validation - A Theoretical Issue? In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 23–42. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Freytag, T.: Softwarevalidierung durch Auswertung von Petrinetz-Abläufen. Dissertation, Karlsruhe (2001)

    Google Scholar 

  9. Ford Jr., L.R., Fulkerson, D.R.: Maximal Flow Through a Network. Canadian Journal of Mathematics 8, 399–404 (1955)

    Article  MathSciNet  Google Scholar 

  10. Karzanov, A.V.: Determining the Maximal Flow in a Network by the Method of Preflows. Soviet Math. Doc. 15, 434–437 (1974)

    MATH  Google Scholar 

  11. Goldberg, A., Rao, S.: Beyond the Flow Decomposition Barrier. Journal of the ACM 45(5), 783–797 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  12. Goltz, U., Reisig, W.: The Non-Sequential Behaviour of Petri Nets. Information and Control 57(2-3), 125–147 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  13. Goltz, U., Reisig, W.: Processes of Place/Transition Nets. LNCS, vol. 154, pp. 264–277. Springer, Heidelberg (1983)

    Google Scholar 

  14. Schröter, C., Schwoon, S., Esparza, J.: The Model-Checking Kit. LNCS, vol. 2676, pp. 463–472. Springer, Heidelberg (2003)

    Google Scholar 

  15. http://theoretica.informatik.uni-oldenburg.de/~pep/

  16. http://www.fmi.uni-stuttgart.de/szs/tools/mckit/

  17. Harel, D., Kugler, H., Pnueli, A.: Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 309–324. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. http://www.wisdom.weizmann.ac.il/~playbook/

  19. http://www.inf.uni-konstanz.de/soft/tools_en.php?sys=1

  20. Ben-Abdallah, H., Leue, S.: MESA: Support for Scenario-Based Design of Concurrent Systems. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 118–135. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  21. Lettrari, M., Klose, J.: Scenario-Based Monitoring and Testing of Real-Time UML Models. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 317–328. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. http://www.osc-es.de/products/en/testconductor.php

  23. Khendek, F., Zhang, X.J.: From MSC to SDL: Overview and an Application to the Autonomous Shuttle Transport System. In: Leue, S., Systä, T.J. (eds.) Scenarios: Models, Transformations and Tools. LNCS, vol. 3466, pp. 228–254. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  24. Mansurov, N.: Automatic synthesis of SDL from MSC and its applications in forward and reverse engineering. Comput. Lang. 27(1), 115–136 (2001)

    Article  MATH  Google Scholar 

  25. Damm, W., Klose, J.: Verification of a Radio-Based Signaling System Using the STATEMATE Verification Environment. Formal Methods in System Design 19(2), 121–141 (2001)

    Article  MATH  Google Scholar 

  26. Klose, J., Wittke, H.: An Automata Based Interpretation of Live Sequence Charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 512–527. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Lehrstuhl für Angewandte Informatik, Katholische Universität Eichstätt-Ingolstadt, Eichstätt, Germany

    Robin Bergenthum, Jörg Desel & Robert Lorenz

  2. Faculty of Electrical Engineering and Information Technology, Slovak University of Technology, Bratislava, Slovakia

    Gabriel Juhás

Authors
  1. Robin Bergenthum
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jörg Desel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gabriel Juhás
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Robert Lorenz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, 10149, Torino, Italy

    Susanna Donatelli

  2. School of Computing, National University of Singapore,  

    P. S. Thiagarajan

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bergenthum, R., Desel, J., Juhás, G., Lorenz, R. (2006). Can I Execute My Scenario in Your Net? VipTool Tells You!. In: Donatelli, S., Thiagarajan, P.S. (eds) Petri Nets and Other Models of Concurrency - ICATPN 2006. ICATPN 2006. Lecture Notes in Computer Science, vol 4024. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11767589_21

Download citation

  • DOI: https://doi.org/10.1007/11767589_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-34699-9

  • Online ISBN: 978-3-540-34700-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation