Verifying UCM specifications of distributed systems using colored Petri nets. (English. Russian original) Zbl 1317.93177
Cybern. Syst. Anal. 51, No. 2, 213-222 (2015); translation from Kibern. Sist. Anal. 2015, No. 2, 62-74 (2015).
Summary: 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.
MSC:
| 93C65 | Discrete event control/observation systems |
Keywords:
verification; specification; distributed system; use case map notation; colored Petri net; SPIN model checkerReferences:
| [1] | D. Amyot and G. Mussbacher, “User requirements notation: The first ten years, The next ten years (Invited Paper),” J. Software, 6, No 5, 747-768 (2011), http://ojs.academypublisher.com/index.php/jsw/article/view/4659. · doi:10.4304/jsw.6.5.747-768 |
| [2] | D. Amyot, M. Weiss, and L. Logrippo, “Generation of test purposes from use case maps,” Computer Networks, 49, No. 5, 643-660 (2009). · doi:10.1016/j.comnet.2005.05.006 |
| [3] | S. N. Baranov, P. D. Drobintsev, V. P. Kotlyarov, and A. A. Letichevsky, “The technology of automated verification and testing in industrial projects,” in: Proc. IEEE Russia Northwest Section, 110 Anniv. of Radio Invention Conf.; IEEE Press, St. Petersburg (2005), pp. 81-89. |
| [4] | S. Baranov, V. Kotlyarov, and T. Weigert, “Verifiable coverage criteria for automated testing,” in: Proc. SDL-Forum 2011; Lect. Notes Comput. Sci., 7083, 79-89 (2011). |
| [5] | J. Hassine, J. Rilling, and R. Dssouli, “Use case maps as a property specification language,” Software and Systems Modeling, 8, No. 2, 205-220 (2009). · doi:10.1007/s10270-007-0076-6 |
| [6] | ITU-T, Recommendation Z.151 (10/12), User Requirements Notation (URN) — Language definition, http://www.itu.int/rec/T-REC-Z.151/en. |
| [7] | jUCMNav: An Extension of the Eclipse Integrated Development Environment for Supporting User Requirements Notation, http://jucmnav.softwareengineering.ca/ ucm/bin/view/ProjetSEG/WebHome. |
| [8] | J. Hassine, J. Rilling, and R. Dssouli, “Abstract operational semantics for use case maps,” in: Proc. FORTE 2005; Lect. Notes Comput. Sci., 3731, 366-380 (2005). · Zbl 1169.68505 |
| [9] | J. Hassine, J. Rilling, and R. Dssouli, “Formal verification of use case maps with real time extensions,” in: Proc. SDL-Forum 2007; Lect. Notes Comput. Sci., 4745, 225-241 (2007). |
| [10] | I. S. Anureev, S. N. Baranov, D. M. Beloglazov, E. V. Bodin, P. D. Drobintsev, and A. V. Kolchin, V. P. Kotlyarov, A. A. Letichevsky, O. A. Letychevskyi, V. A. Nepomniaschy, I. V. Nikiforov, S. V. Potiyenko, L. V. Priyma, and B. V. Tyutin, “Tools for supporting an integrated technology for the analysis and verification of specifications of telecommunication applications,” in: Trans. SPIIRAS, St. Petersburg, 26, No. 1 (2013), pp. 349-383. |
| [11] | S. Baranov, J. Kapitonova, A. Letichevsky, V. Volkov, and T. Weigert, “Basic protocols, message sequence charts, and verification of requirements specifications,” Computer Networks, 49, No. 5, 661-675 (2005). · Zbl 1101.68375 · doi:10.1016/j.comnet.2005.05.005 |
| [12] | K. Jensen and L. M. Kristensen, Colored Petri Nets: Modeling and Validation of Concurrent Systems, Springer, Berlin (2009). · Zbl 1215.68153 · doi:10.1007/b95112 |
| [13] | G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, Boston (2004). |
| [14] | N. V. Vizovitin, V. A. Nepomniaschy, and A. A. Stenenko, “Verification of UCM specifications of distributed systems using colored Petri nets,” in: Proc. IV Intern. Workshop PSSV 2013, Yaroslavl (2013), pp. 70-80. · Zbl 1317.93177 |
| [15] | N. V. Vizovitin and V. A. Nepomniaschy, Algorithms for Translating UCM Specifications into Colored Petri Nets [in Russian], Prepr. 168, A. P. Ershov Institute of Informatics Systems of SB RAS, Novosibirsk (2012), http://www.iis.nsk.su/files/preprints/168.pdf. · Zbl 1317.93177 |
| [16] | N. V. Vizovitin, “Verification of UCM specifications of distributed systems using colored Petri nets. Appendix,” http://bitbucket.org/vizovitin/ucm-verification-examples. · Zbl 1317.93177 |
| [17] | CPN Tools for Editing, Simulating, and Analyzing Colored Petri Nets, http://cpntools.org/. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
