caa a22 4500 605519285 CHVBK 20210128100729.0 cr unu---uuuuu 210128e20150301xx s 000 0 eng 10.1007/s10559-015-9714-0 doi (NATIONALLICENCE)springer-10.1007/s10559-015-9714-0 Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets [Elektronische Daten] [N. Vizovitin, V. Nepomniaschy, A. Stenenko] This article presents a new method for the analysis and verification of Use Case Map (UCM) specifications with the help of colored Petri nets and the SPIN model checker. Standardized UCM notation is a convenient visual language that allows one to formally represent functional requirements. Algorithms for translating UCM specifications into colored Petri nets and colored Petri nets into the input language Promela of the SPIN model checker are described. The complexity of the obtained colored Petri nets is evaluated. The execution of the presented translation algorithms and support tools is illustrated by the example of error localization and correction in the initial UCM specification of a simple network protocol. Springer Science+Business Media New York, 2015 verification nationallicence specification nationallicence distributed system nationallicence Use Case Map notation nationallicence colored Petri net nationallicence SPIN model checker nationallicence Vizovitin N. A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia aut Nepomniaschy V. A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia aut Stenenko A. A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia aut Cybernetics and Systems Analysis Springer US; http://www.springer-ny.com 51/2(2015-03-01), 213-222 1060-0396 51:2<213 2015 51 10559 https://doi.org/10.1007/s10559-015-9714-0 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s10559-015-9714-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Vizovitin N. A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia aut NATIONALLICENCE 700 1- Nepomniaschy V. A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia aut NATIONALLICENCE 700 1- Stenenko A. A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia aut NATIONALLICENCE 773 0- Cybernetics and Systems Analysis Springer US; http://www.springer-ny.com 51/2(2015-03-01), 213-222 1060-0396 51:2<213 2015 51 10559