Skip to main content
SpringerLink
Log in

Application of Colored Petri Nets for Verification of Scenario Control Structures in UCM Notation

  • Published:
Automatic Control and Computer Sciences Aims and scope Submit manuscript

Abstract

The article presents a method for the analysis and verification of Use Case Map (UCM) models with scenario control structures—protected components and failure handling constructs. UCM models are analyzed and verified with the help of colored 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. Anureev, I.S., Baranov, S.N., Beloglazov, D.M., Bodin, E.V., Drobintsev, P.D., Kolchin, A.V., Kotlyarov, V.P., Letichevskii, A.A., Letichevskii, A.A., Jr., Nepomnyashchii, V.A., Nikiforov, I.V., Potienko, S.V., Priima, L.V., and Tyutin, B.V., Tools of integrated technology for analysis and verification of telecom application specs, SPIIRAS Proc., 2013, vol. 26, pp. 349–383.

    Google Scholar 

  2. Stenenko, A.A. and Nepomniaschy, V.A., Verifikatsiya raskrashennykh setei Petri metodom proverki modelei, Preprint 178 (Model Checking Approach to Verification of Coloured Petri Nets, Preprint 178), Novosibirsk: Inst. sist. inf. SO RAN, 2015. http://www.iis.nsk.su/files/preprints/stenenkoffnepomniaschyff178.pdf.

    Google Scholar 

  3. Vizovitin, N.V. and Nepomniaschy, V.A., Algoritmy translyatsii UCM-spetsifikatsii v raskrashennye seti Petri, Preprint 168 (UCM-Specifications to Colored Petri Nets Translation Algorithms, Preprint 168), Novosibirsk: Inst. sist. inf. SO RAN, 2012. http://www.iis.nsk.su/files/preprints/168.pdf.

    Google Scholar 

  4. Kotlyarov, V. and Weigert, T., Verifiable coverage criteria for automated testing, Lect. Notes Comput. Sci., 2011, vol. 7083, pp. 79–89.

    Article  Google Scholar 

  5. Baranov, S.N., Drobintsev, P.D., Kotlyarov, V.P., and Letichevsky, A.A., The technology of automated verification and testing in industrial projects, Proc. IEEE Russia Northwest Section 110 Anniversary of Radio Invention Conference, St. Petersburg, 2005, pp. 81–89.

    Google Scholar 

  6. Boulet, P., Amyot, D., and Stepien, B., Towards the generation of tests in the test description language from use case map models, Lect. Notes Comput. Sci., 2015, vol. 9369, pp. 193–201.

    Article  Google Scholar 

  7. CPN Tools Homepage. http://cpntools.org/.

  8. Hassine, J., Rilling, J., and Dssouli, R., Abstract operational semantics for use case maps, Lect. Notes Comput. Sci., 2005, vol. 3731, pp. 366–380.

    Article  MATH  Google Scholar 

  9. Hassine, J., Early modeling and validation of timed system requirements using Timed Use Case Maps, Requir. Eng., 2015, vol. 20, no. 2, pp. 181–211.

    Article  Google Scholar 

  10. Hassine, J., Rilling, J., and Dssouli, R., Use case maps as a property specification language, Software Syst. Model., 2009, vol. 8, no. 2, pp. 205–220.

    Article  MATH  Google Scholar 

  11. Holzmann, G.J., The SPIN Model Checker. Primer and Reference Manual, Addison-Wesley, 2004.

    Google Scholar 

  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. and Kristensen, L.M., Coloured Petri Nets: Modelling and Validation of Concurrent Systems, Springer, 2009.

    Book  MATH  Google Scholar 

  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., and Stenenko, A.A., Verifying UCM specifications of distributed systems using colored Petri nets, Cybern. Syst. Anal., 2015, vol. 51, no. 2, pp. 213–222.

    Article  MATH  Google Scholar 

  17. Vizovitin, N.V., Nepomniaschy, V.A., and Stenenko, A.A., Verification of UCM models with scenario control structures using colored Petri nets, Syst. Inf., 2016, vol. 7, pp. 11–22.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Ershov Institute of Informatics Systems, Siberian Branch, Russian Academy of Sciences, Novosibirsk, 630090, Russia

    N. V. Vizovitin, V. A. Nepomniaschy & A. A. Stenenko

Authors
  1. N. V. Vizovitin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. V. A. Nepomniaschy
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. A. A. Stenenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to N. V. Vizovitin.

Additional information

Original Russian Text © N.V. Vizovitin, V.A. Nepomniaschy, A.A. Stenenko, 2016, published in Modelirovanie i Analiz Informatsionnykh Sistem, 2016, Vol. 23, No. 6, pp. 688–702.

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Vizovitin, N.V., Nepomniaschy, V.A. & Stenenko, A.A. Application of Colored Petri Nets for Verification of Scenario Control Structures in UCM Notation. Aut. Control Comp. Sci. 51, 489–497 (2017). https://doi.org/10.3103/S0146411617070227

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.3103/S0146411617070227

Keywords

Search

Navigation