Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation
https://doi.org/10.18255/1818-1015-2016-6-688-702
Abstract
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.
Keywords
About the Authors
N. V. Vizovitin
A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences
Russian Federation
Russian Federation
junior researcher, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia
V. A. Nepomniaschy
A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences
Russian Federation
PhD, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia
Russian Federation
PhD, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia
A. A. Stenenko
A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences
Russian Federation
graduate student, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia
Russian Federation
graduate student, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia
References
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 178, http://www.iis.nsk.su/files/preprints/stenenko_nepomniaschy_178.pdf, Institute of Infornatics Systems RAS, Novosibirsk, 2015, 28 pp., in Russian.
3. Vizovitin N.V., Nepomniaschy V.A., UCM-Specifications to Colored Petri Nets Translation Algotithms, Preprint 168, http://www.iis.nsk.su/files/preprints/168. pdf, 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, 2005, 366–380.
9. Hassine J. Early modeling and validation of timed system requirements using Timed Use Case Maps, Requirements Engineering, 20:2 (2015), 181–211.
10. Hassine J., Rilling J., Dssouli R, “Use Case Maps as a Property Specification Language”, Software and Systems Modeling, 8:2 (2009), 205–220.
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.
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.
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.
Review
For citations:
Vizovitin N.V., Nepomniaschy V.A., Stenenko A.A. Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation. Modeling and Analysis of Information Systems. 2016;23(6):688-702. (In Russ.) https://doi.org/10.18255/1818-1015-2016-6-688-702
Views:
2908
Email this article 