Application of coloured Petri nets for verification of scenario control structures in UCM notation

N. V. Vizovitin ; V. A. Nepomniaschy ; A. A. Stenenko

Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 688-702.

Résumé

This article presents a method for the analysis and verification of Use Case Maps (UCM) models with scenario control structures — protected components and failure handling constructs. UCM models are analyzed and verified with the help of coloured Petri nets (CPN) and the SPIN model checker. Algorithms for translating UCM scenario control structures into CPN and CPN into SPIN input language Promela are described. The number of elements of the resulting CPN model and the number of Promela model states are estimated. The presented algorithm and the verification process are illustrated by the study of a network router firmware update.

Détail

Keywords: verification, translation, coloured Petri nets, SPIN, protected component, error handling.
Mots-clés : UCM

Bibliographie

[1] Anureev I. S., Baranov S. N., Beloglazov D. M., Bodin E. V., Drobitsev P. D., Kolchin A. V., Kotlyarov V. P., Letichevsky A. A., Letichevsky A. A. jr., Nepomniaschy V. A., Nikiforov I. V., Potiyenko S. V., Priyma L. V., Tyutin B. V., “Tools of Integrated Technology for Analysis and Verication of Telecom Application Specs”, SPIIRAS Proceedings, 26 (2013), 349–383 (in Russian)

[2] Stenenko A. A., Nepomniaschy V. A., Model Checking Approach to Verifiaction of Coloured Petri Nets, Preprint No 178, Institute of Infornatics Systems RAS, Novosibirsk, 2015, 28 pp. (in Russian) | Zbl

[3] Vizovitin N. V., Nepomniaschy V. A., UCM-Specifications to Colored Petri Nets Translation Algotithms, Preprint No 168, Institute of Infornatics Systems RAS, Novosibirsk, 2012, 55 pp. (in Russian)

[4] Kotlyarov V., Weigert T., “Verifiable Coverage Criteria for Automated Testing”, SDL 2011, LNSC, 7083, 2011, 79–89

[5] Baranov S. N., Drobintsev P. D., Kotlyarov V. P., Letichevsky A. A., “The Technology of Automated Verification and Testing in Industrial Projects”, Proc. IEEE Russia Northwest Section, 110 Anniversary of Radio Invention Conference, IEEE Press, St. Petersburg, 2005, 81–89

[6] Boulet P., Amyot D., Stepien B., “Towards the Generation of Tests in the Test Description Language from Use Case Map Models”, SDL 2015, LNCS, 9369, Springer, 2015, 193–201

[7] CPN Tools Homepage, http://cpntools.org/

[8] Hassine J., Rilling J., Dssouli R., “Abstract Operational Semantics for Use Case Maps”, FORTE 2005, LNCS, 3731, Springer, 2005, 366–380 | Zbl

[9] Hassine J., “Early modeling and validation of timed system requirements using Timed Use Case Maps”, Requirements Engineering, 20:2 (2015), 181–211 | DOI

[10] Hassine J., Rilling J., Dssouli R., “Use Case Maps as a Property Specification Language”, Software and Systems Modeling, 8:2 (2009), 205–220 | DOI | MR

[11] Holzmann G. J., The SPIN model checker. Primer and Reference Manual, Addison-Wesley, 2004

[12] ITU-T, Recommendation Z.151 (10/12), User Requirements Notation (URN) — Language definition, http://www.itu.int/rec/T-REC-Z.151/en

[13] jUCMNav — Eclipse plugin for the User Requirements Notation, http://jucmnav.softwareengineering.ca/ucm/bin/view/ProjetSEG/WebHome

[14] Jensen K., Kristensen L. M., Coloured Petri Nets: Modelling and Validation of Concurrent Systems, Springer, 2009 | MR

[15] Vizovitin N. V., Application of coloured Petri nets for verification of scenario control structures in UCM notation. Appendix, http://bitbucket.org/vizovitin/ucm-verification-examples-3

[16] Vizovitin N. V., Nepomniaschy V. A., Stenenko A. A., “Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets”, Cybernetics and Sys. Anal., 51:2 (2015), 213–222 | DOI | Zbl

[17] Vizovitin N. V., Nepomniaschy V. A., Stenenko A. A., “Verification of UCM Models with Scenario Control Structures Using Colored Petri Nets”, System Informatics, 7 (2016), 11–22