×

Oclets – scenario-based modeling with Petri nets. (English) Zbl 1242.68176

Franceschinis, Giuliana (ed.) et al., Applications and theory of Petri nets. 30th international conference, PETRI NETS 2009, Paris, France, June 22–26, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02423-8/pbk). Lecture Notes in Computer Science 5606, 223-242 (2009).
Summary: We present a novel, operational, formal model for scenario-based modeling with Petri nets. A scenario-based model describes the system behavior in terms of partial runs, called scenarios. This paradigm has been formalized in message sequence charts (MSCs) and live sequence charts (LSCs) which are in industrial and academic use. A particular application for scenarios are process models in disaster management where system behavior has to be adapted frequently, occasionally at run-time. An operational semantics of scenarios would allow to execute and adapt such systems on a formal basis.
In this paper, we present a class of Petri nets for specifying and modeling systems with scenarios and anti-scenarios. We provide an operational semantics allowing to iteratively construct partially ordered runs that satisfy a given specification. We prove the correctness of our results.
For the entire collection see [Zbl 1165.68011].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q55 Semantics in the theory of computing

Software:

VipTool
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Form. Methods Syst. Des. 19(1), 45–80 (2001) · Zbl 0985.68033 · doi:10.1023/A:1011227529550
[2] Desel, J.: From human knowledge to process models. In: UNISCON, pp. 84–95 (2008) · doi:10.1007/978-3-540-78942-0_10
[3] Fahland, D., Woith, H.: Towards process models for disaster response. In: Ardagna, D., et al. (eds.) BPM 2008 Workshops. LNBIP, vol. 17, pp. 244–256. Springer, Heidelberg (2008)
[4] Mukund, M., Kumar, K.N., Thiagarajan, P.S.: Netcharts: Bridging the gap between HMSCs and executable specifications. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 293–307. Springer, Heidelberg (2003) · Zbl 1274.68198 · doi:10.1007/978-3-540-45187-7_20
[5] Mauw, S., Reniers, M.A.: An algebraic semantics of Basic Message Sequence Charts. The Computer Journal 37, 269–277 (1994) · Zbl 05479061 · doi:10.1093/comjnl/37.4.269
[6] Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 1–33. Springer, Heidelberg (2001) · Zbl 0989.68087 · doi:10.1007/3-540-44674-5_1
[7] Hélouët, L., Jard, C., Caillaud, B.: An event structure based semantics for high-level message sequence charts. Mathematical. Structures in Comp. Sci. 12(4), 377–402 (2002) · Zbl 1009.68070
[8] Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991) · Zbl 0743.68106 · doi:10.1007/BF01463946
[9] Reisig, W.: Elements Of Distributed Algorithms: Modeling and Analysis with Petri Nets. Springer, Heidelberg (1998) · Zbl 0907.68130 · doi:10.1007/978-3-662-03687-7
[10] Esparza, J., Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. Springer, Heidelberg (2008) · Zbl 1153.68035
[11] Kluge, O.: Petri nets as a semantic model for Message Sequence Chart specifications. In: INT 2002, Grenoble, France, pp. 138–147 (2002)
[12] Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002) · Zbl 1019.68622 · doi:10.1007/3-540-36126-X_23
[13] Desel, J., Juhás, G., Lorenz, R., Neumair, C.: Modelling 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) · doi:10.1007/3-540-44895-0_26
[14] Bergenthum, R., Desel, J., Lorenz, R., Mauser, S.: Synthesis of Petri Nets from Finite Partial Languages. Fundam. Inform. 88(4), 437–468 (2008) · Zbl 1167.68037
[15] Bergenthum, R., Mauser, S.: Synthesis of Petri Nets from Infinite Partial Languages with VipTool. In: AWPN 2008, Rostock, Germany, University of Rostock (September 2008) · Zbl 1167.68037
[16] Hee, K., Serebrenik, A., Sidorova, N., Voorhoeve, M., Werf, J.: Modelling with History-Dependent Petri Nets. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 320–327. Springer, Heidelberg (2007) · Zbl 05319453 · doi:10.1007/978-3-540-75183-0_23
[17] Barros, J.a.P., Gomes, L.: Net model composition and modification by net operations: a pragmatic approach. In: Proceedings of INDIN 2004, Berlin, Germany (June 2004) · doi:10.1109/INDIN.2004.1417350
[18] Rinderle, S., Reichert, M., Dadam, P.: Evaluation of correctness criteria for dynamic workflow changes. In: van der Aalst, W.M.P., ter Hofstede, A.H.M., Weske, M. (eds.) BPM 2003. LNCS, vol. 2678, pp. 41–57. Springer, Heidelberg (2003) · doi:10.1007/3-540-44895-0_4
[19] Ehrig, H., Hoffmann, K., Padberg, J., Prange, U., Ermel, C.: Independence of net transformations and token firing in reconfigurable place/transition systems. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 104–123. Springer, Heidelberg (2007) · Zbl 1226.68052 · doi:10.1007/978-3-540-73094-1_9
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.