Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605519285 | ||
| 003 | CHVBK | ||
| 005 | 20210128100729.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150301xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s10559-015-9714-0 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s10559-015-9714-0 | ||
| 245 | 0 | 0 | |a Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets |h [Elektronische Daten] |c [N. Vizovitin, V. Nepomniaschy, A. Stenenko] |
| 520 | 3 | |a 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. | |
| 540 | |a Springer Science+Business Media New York, 2015 | ||
| 690 | 7 | |a verification |2 nationallicence | |
| 690 | 7 | |a specification |2 nationallicence | |
| 690 | 7 | |a distributed system |2 nationallicence | |
| 690 | 7 | |a Use Case Map notation |2 nationallicence | |
| 690 | 7 | |a colored Petri net |2 nationallicence | |
| 690 | 7 | |a SPIN model checker |2 nationallicence | |
| 700 | 1 | |a Vizovitin |D N. |u A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia |4 aut | |
| 700 | 1 | |a Nepomniaschy |D V. |u A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia |4 aut | |
| 700 | 1 | |a Stenenko |D A. |u A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia |4 aut | |
| 773 | 0 | |t Cybernetics and Systems Analysis |d Springer US; http://www.springer-ny.com |g 51/2(2015-03-01), 213-222 |x 1060-0396 |q 51:2<213 |1 2015 |2 51 |o 10559 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s10559-015-9714-0 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s10559-015-9714-0 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Vizovitin |D N. |u A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Nepomniaschy |D V. |u A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Stenenko |D A. |u A. P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Science, Novosibirsk, Russia |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Cybernetics and Systems Analysis |d Springer US; http://www.springer-ny.com |g 51/2(2015-03-01), 213-222 |x 1060-0396 |q 51:2<213 |1 2015 |2 51 |o 10559 | ||