Geodesic
Application of coloured Petri nets for verification of scenario control structures in UCM notation
Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 688-702

Voir la notice de l'article provenant de la source Math-Net.Ru

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: verification, translation, coloured Petri nets, SPIN, protected component, error handling.
Mots-clés : UCM 
@article{MAIS_2016_23_6_a1,
     author = {N. V. Vizovitin and V. A. Nepomniaschy and A. A. Stenenko},
     title = {Application of coloured {Petri} nets for verification of scenario control structures in {UCM} notation},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {688--702},
     publisher = {mathdoc},
     volume = {23},
     number = {6},
     year = {2016},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a1/}
}
TY  - JOUR
AU  - N. V. Vizovitin
AU  - V. A. Nepomniaschy
AU  - A. A. Stenenko
TI  - Application of coloured Petri nets for verification of scenario control structures in UCM notation
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2016
SP  - 688
EP  - 702
VL  - 23
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a1/
LA  - ru
ID  - MAIS_2016_23_6_a1
ER  - 
%0 Journal Article
%A N. V. Vizovitin
%A V. A. Nepomniaschy
%A A. A. Stenenko
%T Application of coloured Petri nets for verification of scenario control structures in UCM notation
%J Modelirovanie i analiz informacionnyh sistem
%D 2016
%P 688-702
%V 23
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a1/
%G ru
%F MAIS_2016_23_6_a1
N. V. Vizovitin; V. A. Nepomniaschy; A. A. Stenenko. Application of coloured Petri nets for verification of scenario control structures in UCM notation. Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 688-702. http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a1/