nach oben

Software and Systems Modeling

Erschienen in:

02.01.2016 | Regular Paper

Model checking multi-level and recursive nets

verfasst von: Mirtha Lina Fernández Venero, Flávio Soares Corrêa da Silva

Erschienen in: Software and Systems Modeling | Ausgabe 4/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

With the increasing complexity of the problems and systems arising nowadays, the use of multi-level models is becoming more frequent in practice. However, there are still few reports in the literature concerning methods for analyzing such models without flattening the multi-level structure. For instance, several variants of multi-level Petri nets have been applied for modeling interaction protocols and mobility in multi-agent systems and coordination of cross-organizational workflows. But there are few automated tools for analyzing the behavior of these nets. In this paper we explain how to detect faults in models based on a representative class of multi-level nets: the nested Petri nets. We translate a nested net into a verifiable model that preserves its modular structure, a PROMELA program. This allows the use of SPIN model checker to verify properties related to termination, boundedness and reachability.

Vorheriger Artikel Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols

Nächster Artikel On the formal interpretation and behavioural consistency checking of SysML blocks

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

See the complete grammar at http://spinroot.com/spin/Man/grammar.html.

The skip statement is equivalent to the constant 1, i.e., it is always executable.

The rendezvous communication in PROMELA is not suitable for simulating the synchronizations in a NPN. A rendezvous statement can only be executed if a matching statement can be performed immediately; otherwise the process is blocked. This would prevent a net token from firing any other transition until the synchronization could be completed.

In case \(np=onp\), transpNetTok is not required. Besides, if t is unlabeled the entire code can be omitted. Also note that net-typed variables do not need a representation in the translation.

An inhibitor arc is enabled when the input place is empty.

Any sequence \(A_k\) may contain regions with priorities 4 or 5, not both.

See http://www.dropbox.com/s/uloj2xmgwomimqv/exNPNMASimpExt.pml?dl=0.

See http://www.dropbox.com/s/28j8x7fhyx7ucdg/npn2cpn.rar?dl=0 for the models.

Error: value (256->0 (8)) truncated in assignment.

See http://www.dropbox.com/s/n7y5ib76ym9x59p/exNPNMASsmall.pml?dl=0.

The first verification of the model may use the standard PROMELA receive statement, instead of the non-deterministic version.

Augusto, J., Butler, M., Ferreira, C., Craig, S.: Using SPIN and STeP to verify business processes specifications. Perspect. Syst. Inform. LNCS 2890, 207–213 (2003)CrossRef

Barkaoui, K., Hicheur, A.: Towards analysis of flexible and collaborative workflow using recursive ECATN ets. In: ter Hofstede, A., Benatallah, B., Paik, H.-Y. (eds.) Business Process Management Workshops, LNCS, vol. 4928, pp. 232–244. Springer, Berlin, Heidelberg (2008)

Bednarczyk, M.A., Bernardinello, L., Pawlowski, W., Pomello, L.: Modelling mobility with Petri hypernets. In: Proceedings of 17th International Conference on Recent Trends in Algebraic Development Techniques, WADT’04, pp. 28–44 (2005)

Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder-second generation of a Java model checker. In: Workshop on Advances in Verification (2000)

Cabac, L., Duvigneau, M., Moldt, D., Rölke, H.: Modeling dynamic architectures using nets-within-nets. In: Proceedings of International Conference on Applications and Theory of Petri Nets, LNCS, vol. 3536, pp. 148–167 (2005)

Ceška, M., Janoušek, V., Vojnar, T.: PNtalk—a computerized tool for object oriented Petri nets modelling. In: Computer Aided Systems Theory (EUROCAST’97), LNCS, vol. 1333, pp. 591–610. Springer, Berlin (1997)

Chang, L., He, X.: A model transformation approach for verifying multi-agent systems using SPIN. In: Proceedings ACM Symposium on Applied Computing, pp. 37–42 (2011)

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The maude 2.0 system. In: Proceedings of 14th International Conference on Rewriting Techniques and Applications, LNCS, vol. 2706, pp. 76–87 (2003)

Dworzański, L., Lomazova, I.: CPN tools-assisted simulation and verification of nested Petri nets. Autom. Control Comput. Sci. 47(7), 393–402 (2013)CrossRef

10.

Eker, S., Meseguer, J., Sridharanarayanan, A.: The maude LTL model checker. In: Proceedings Workshop on Rewriting Logic and Its Applications, ENTCS, vol. 71, pp. 162–187 (2002)

11.

Eshuis, R.: Symbolic model checking of UML activity diagrams. ACM Trans. Softw. Eng. Methodol. 15(1), 1–38 (2006)CrossRef

12.

Farwer, B., Leuschel, M.: Model checking object Petri nets in Prolog. In: Proceedings 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 20–31 (2004)

13.

Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R., Ouenzar, M.: Comparison of model checking tools for information systems. In: Proceedings 12th International Conference on Formal Engineering Methods and Software Engineering, pp. 581–596 (2010)

14.

Gallardo, M.M., Merino, P., Pimentel, E.: A generalized semantics of PROMELA for abstract model checking. Form. Asp. Comput. 16(3), 166–193 (2004)CrossRefMATH

15.

Gannod, G.C., Gupta, S.: An automated tool for analyzing Petri nets using SPIN. In: Proceedings of 16th IEEE International Conference on Automated Software Engineering, pp. 404–407. IEEE Computer Society (2001)

16.

Grahlmann, B., Pohl, C.: Profiting from SPIN in PEP. In: SPIN Workshop (1998)

17.

Haddad, S., Poitrenaud, D.: Recursive Petri nets-theory and application to discrete event systems. Acta Inform. 44(7–8), 463–508 (2007)MathSciNetCrossRefMATH

18.

Hicheur, A., Ben Dhieb, A., Barkaoui, K.: Modelling and analysis of flexible healthcare processes based on algebraic and recursive Petri nets. In: Weber, J., Perseil, I. (eds.) Foundations of Health Information Engineering and Systems, LNCS, vol. 7789, pp. 1–18. Springer, Berlin, Heidelberg (2013)

19.

Hillah, L., Kordon, F., Petrucci, L., Trèves, N.: PNML framework: an extendable reference implementation of the Petri net markup language. In: Proceedings of International Conference on Applications and Theory of Petri Nets, LNCS, vol. 6128, pp. 318–327 (2010)

20.

Holzmann, G.J.: Tutorial: design and validation of protocols. Tutor. Comput. Netw. ISDN Syst. 25, 981–1017 (1991)CrossRef

21.

Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRef

22.

Holzmann, G.J.: An analysis of bitstate hashing. Form. Methods Syst. Des. 13(3), 289–307 (1998)MathSciNetCrossRef

23.

Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)

24.

Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques, pp. 197–211 (1995)

25.

Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Springer, Berlin (1992)CrossRefMATH

26.

Jensen, K., Kristensen Rozenberg, L. (eds.): Coloured Petri Nets—Modeling and Validation of Concurrent Systems. Springer, Berlin (2009)

27.

Jensen, K., Rozenberg, G. (eds.): High-Level Petri Nets: Theory and Application. Springer, Berlin (1991)MATH

28.

Kissoum, Y., Sahnoun, Z.: A recursive colored Petri nets semantics for AUML as base of test case generation. In: Proceedings IEEE/ACS International Conference on Computer Systems and Applications, pp. 785–792 (2008)

29.

Koch, I.: Petri nets in systems biology. Softw. Syst. Model. 14(2), 703–710 (2015)CrossRef

30.

Köhler, M., Moldt, D., Rölke, H.: Modelling mobility and mobile agents using nets within nets. ICATPN, LNCS 2679, 121–139 (2003)MathSciNet

31.

Kummer, O., Wienberg, F., Duvigneau, M., Schumacher, J., Köhler, M., Moldt, D., Rölke, H., Valk, R.: An extensible editor and simulation engine for Petri nets: Renew. In: Proceedings of International Conference on Applications and Theory of Petri Nets, LNCS, vol. 3099, pp. 484–493 (2004)

32.

Lakos, C.: From coloured Petri nets to object Petri nets. In: ICATPN, LNCS, pp. 278–297. Springer, Berlin (1995)

33.

Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Form. Asp. Comput. 11(6), 637–664 (1999)CrossRefMATH

34.

Lehmann K., Cabac, L., Moldt, D., Rölke H.: Towards a distributed tool platform based on mobile agents. In: Eymann, T., Klügl, F., Lamersdorf, W., Klusch, M., Huhns, M.N. (eds.) Multiagent System Technologies. LNCS, vol. 3550, pp. 179–190. Springer, Berlin, Heidelberg (2005)

35.

Leuschel, M., Massart, T.: Logic programming and partial deduction for the verification of reactive systems: an experimental evaluation. In: Proceedings 2nd Workshop on Automated Verification of Critical Systems, pp. 143–150 (2002)

36.

Leyla, N., Mashiyat, A.S., Wang, H., MacCaull, W.: Towards workflow verification. In: Proceedings Conference of the Center for Advanced Studies on Collaborative Research, pp. 253–267 (2010)

37.

Lomazova, I.A.: Nested Petri nets—a formalism for specification and verification of multi-agent distributed systems. Fundam. Inf. 43(1–4), 195–214 (2000)MathSciNetMATH

38.

Lomazova, I.A.: Nested Petri nets: multilevel and recursive systems. Fundam. Inf. 47, 283–293 (2001)MATH

39.

Lomazova, I.A.: Recursive nested Petri nets: analysis of semantic properties and expressibility. Program. Comput. Softw. 27(4), 183–193 (2001)MathSciNetCrossRefMATH

40.

Lomazova, I.A.: Modeling dynamic objects in distributed systems with nested Petri nets. Fundam. Inf. 51(1–2), 121–133 (2002)MathSciNetMATH

41.

Lomazova, I.A.: Nested Petri nets for adaptive process modeling. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science, LNCS, vol. 4800, pp. 460–474. Springer, Berlin, Heidelberg (2008)

42.

Lomazova, I.A., Schnoebelen, P.: Some decidability results for nested Petri nets. In: 3rd International Andrei Ershov Memorial Conference Perspectives of System Informatics’99, LNCS, vol. 1755, pp. 208–220 (2000)

43.

Mascheroni, M., Farina, F.: Nets-within-nets paradigm and grid computing. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V, LNCS, vol. 6900, pp. 201–220. Springer, Berlin, Heidelberg (2012)

44.

Mateescu, R., Garavel, H.: XTL: a meta-language and tool for temporal logic model-checking. In: Proceedings of International Workshop on Software Tools for Technology Transfer, BRICS, pp. 33–42 (1998)

45.

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

46.

Natarajan, V., Holzmann, G.J.: Outline for an operational semantics of PROMELA. In: The SPIN Verification System. Proceedings of the 2nd SPIN Workshop 1996, DIMACS-Discrete Mathematics and Theoretical Computer Science, vol. 32 (1997)

47.

Prisecaru, O., Jucan, T.: Interorganizational workflow nets: a Petri net based approach for modelling and analyzing interorganizational workflows. In: EOMAS, pp. 64–78 (2008)

48.

Ratzer, A., Wells, L., Lassen, H., Laursen, M., Qvortrup, J., Stissing, M., Westergaard, M., Christensen, S., Jensen, K.: CPN tools for editing, simulating, and analysing coloured Petri nets. In: Proceedings of the International Conference on Applications and Theory of Petri Nets, LNCS, vol. 2679, pp. 450–462 (2003)

49.

Regis, G., Ricci, N., Aguirre, N., Maibaum, T.: Specifying and verifying declarative fluent temporal logic properties of workflows. In: 15th Brazilian Symposium on Formal Methods, LNCS, vol. 7498, pp. 147–162 (2012)

50.

Reisig, W. (ed.): Elements of Distributed Algorithms: Modeling and Analysis with Petri nets. Springer, Berlin (1998)MATH

51.

Ribeiro, L., dos Santos, O., Dotti, F., Foss, L.: Correct transformation: from object-based graph grammars to PROMELA. Sci. Comput. Program. 77(3), 214–246 (2012)CrossRefMATH

52.

Ribeiro, O., Fernandes, J.: Translating synchronous Petri nets into PROMELA for verifying behavioural properties. In: International Symposium on Industrial Embedded Systems, pp. 266–273 (2007)

53.

Ribeiro, O., Fernandes, J., Pinto, L.: Model checking embedded systems with PROMELA. In: IEEE International Conference Engineering of Computer-Based Systems, pp. 378–385 (2005)

54.

Ruys, T.C., Holzmann, G.J.: Advanced SPIN tutorial. In: 11th International SPIN Workshop Model Checking Software, pp. 304–305 (2004)

55.

Sbai, Z., Missaoui, A., Barkaoui, K., Ben Ayed, R.: On the verification of business processes by model checking techniques. In: Proceedings of the 2nd International Conference on Software Technology and Engineering, vol. 1 (2010)

56.

Seghrouchni, A.F., Haddad, S.: A recursive model for distributed planning. In: Proceedings of International Conference on Multi-Agent Systems, pp. 307–314 (1996)

57.

Szpyrka, M., Biernacka, A., Biernacki, J.: Methods of translation of Petri nets to NuSMV language. In: Proceedings of 23rd Workshop on Concurrency, Specification and Programming, pp. 245–256 (2014)

58.

van der Aalst, W.M.P.: Business process management as the Killer App for Petri nets. Softw. Syst. Model. 14(2), 685–691 (2015)CrossRef

59.

Valk, R.: Petri nets as token objects: an introduction to elementary object nets. In: ICATPN, vol. 1420, pp. 1–25 (1998)

60.

Valk, R.: Object Petri nets: using the nets-within-nets paradigm. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, LNCS, vol. 3098, pp. 819–848. Springer, Berlin, Heidelberg (2004)

61.

Venero, M.: Verifying cross-organizational workflows over multi-agent based environments. In: Barjis, J., Pergl, R. (eds.) Enterprise and Organizational Modeling and Simulation, LNBIP, vol. 191, pp. 38–58. Springer, Berlin, Heidelberg (2014)

62.

Venero, M.L.F., da Silva, F.S.C.: On the use of SPIN for studying the behavior of Nested Petri nets. In: Iyoda, J., de Moura, L. (eds.) Formal Methods: Foundations and Applications. LNCS, vol. 8195, pp. 83–98. Springer, Berlin, Heidelberg (2013)

63.

Weise, C.: An incremental formal semantics for PROMELA. In: Proceedings of 3rd International SPIN Workshop (1997)

64.

Yamaguchi, S., Yamaguchi, M., Tanaka, M.: A soundness verification tool based on the SPIN model checker for acyclic workflow nets. In: Proceedings of 23rd International Conference on Circuits/Systems, Computers and Communications, pp. 285–288 (2008)

Titel: Model checking multi-level and recursive nets
verfasst von: Mirtha Lina Fernández Venero
Flávio Soares Corrêa da Silva
Publikationsdatum: 02.01.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: Software and Systems Modeling / Ausgabe 4/2017
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI: https://doi.org/10.1007/s10270-015-0509-6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2017

On the formal interpretation and behavioural consistency checking of SysML blocks

The importance of flow in software development

From software extensions to product lines of dataflow programs

Process mining using BPMN: relating event logs and process models

FLAME: a formal framework for the automated analysis of software product lines validated by automated specification testing

Variability extraction and modeling for product variants