{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T03:07:17Z","timestamp":1775012837587,"version":"3.50.1"},"reference-count":23,"publisher":"Pleiades Publishing Ltd","issue":"6","license":[{"start":{"date-parts":[[2008,11,1]],"date-time":"2008-11-01T00:00:00Z","timestamp":1225497600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2008,11,1]],"date-time":"2008-11-01T00:00:00Z","timestamp":1225497600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2008,11]]},"DOI":"10.1134\/s0361768808060042","type":"journal-article","created":{"date-parts":[[2008,11,22]],"date-time":"2008-11-22T00:55:14Z","timestamp":1227315314000},"page":"330-340","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Modeling and verification of the SDL-specified communication protocols using high-level Petri nets"],"prefix":"10.1134","volume":"34","author":[{"given":"V. A.","family":"Nepomniaschy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V. S.","family":"Argirov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D. M.","family":"Beloglazov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. V.","family":"Bystrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E. A.","family":"Chetvertakov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T. G.","family":"Churina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"137","published-online":{"date-parts":[[2008,11,23]]},"reference":[{"key":"6004_CR1","unstructured":"Specification and Description Language (SDL), Recommendation, Z.100, CCITT 1992."},{"key":"6004_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60794-3","volume-title":"Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use","author":"K. Jensen","year":"1997","unstructured":"Jensen, K., Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Berlin: Springer, 1997, vols. 1\u20133."},{"issue":"2","key":"6004_CR3","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/s100090050021","volume":"2","author":"L.M. Kristensen","year":"1998","unstructured":"Kristensen, L.M., Christensen, S., and Jensen, K., The Practitioner\u2019s Guide to Coloured Petri Nets, Int. J. Software Tools Technology Transfer, 1998, vol. 2, no. 2, pp. 98\u2013132.","journal-title":"Int. J. Software Tools Technology Transfer"},{"key":"6004_CR4","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-44919-1_28","volume":"2679","author":"A.V. Ratzer","year":"2003","unstructured":"Ratzer, A.V., Wells, L., Lassen, H.M., Laursen, A.M., Qvortrup, J.F., Stissing, M.S., Westergaard, M., Christensen, S., and Jensen, K., CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets, in Lecture Notes in Computer Science (Proc. of ICATPN 2003), 2003, vol. 2679, pp. 450\u2013462.","journal-title":"Lecture Notes in Computer Science (Proc. of ICATPN 2003)"},{"key":"6004_CR5","unstructured":"Fisher, J. and Dimitrov, E., Verification of SDL\u201992 Specifications Using Extended Petri Nets, Proc. IFIP Fifteenth Int. Conf. on Protocol Specification, Testing and Verification, Warsaw, 1995, pp. 455\u2013458."},{"key":"6004_CR6","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-69108-1_9","volume":"1420","author":"H. Fleischhack","year":"1998","unstructured":"Fleischhack, H. and Grahlmann, B., A Compositional Net Semantics for SDL, in Lecture Notes in Computer Science, 1998, vol. 1420, pp. 144\u2013164.","journal-title":"Lecture Notes in Computer Science"},{"key":"6004_CR7","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/3-540-45075-0_17","volume":"2708","author":"A. Aalto","year":"2003","unstructured":"Aalto, A., Husberg, N., and Varpaaniemi, K., Automatic Formal Model Generation and Analysis of SDL, in Lecture Notes in Computer Science, 2003, vol. 2708, pp. 285\u2013299.","journal-title":"Lecture Notes in Computer Science"},{"key":"6004_CR8","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0054167","volume":"1384","author":"B. Grahlmann","year":"1998","unstructured":"Grahlmann, B., Combining Finite Automata. Parallel Programs and SDL Using Petri Nets, in Lecture Notes in Computer Science, 1998, vol. 1384, pp. 102\u2013117.","journal-title":"Lecture Notes in Computer Science"},{"key":"6004_CR9","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1007\/3-540-48119-2_36","volume":"1708","author":"N. Husberg","year":"1999","unstructured":"Husberg, N. and Manner, T., Emma: Developing an Industrial Reachability Anallyser for SDL, in Lecture Notes in Computer Science (Proc. of Int. Congress on Formal Methods), 1999, vol. 1708, pp. 642\u2013661.","journal-title":"Lecture Notes in Computer Science (Proc. of Int. Congress on Formal Methods)"},{"key":"6004_CR10","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-74510-5_31","volume":"4649","author":"V.A. Nepomniaschy","year":"2007","unstructured":"Nepomniaschy, V.A., Alekseev, G.I., Argirov, V.S., Beloglazov, D.M., Bystrov A.V., Chetvertakov, E.A., Churina, T.G., Mylnikov, S.P., and Novikov, R.M., Application of Modified Coloured Petri Nets to Modeling and Verification of SDL Specified Communication Protocols, in Lecture Notes in Computer Science (Proc. of CSR 2007), 2007, vol. 4649, pp. 303\u2013314.","journal-title":"Lecture Notes in Computer Science (Proc. of CSR 2007)"},{"issue":"3","key":"6004_CR11","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"Berthomieu, B. and Diaz, M., Modelling and Verification of Time Dependant Systems Using Time Petri Nets, IEEE Trans. Software Eng., 1991, vol. 17, no. 3, pp. 259\u2013273.","journal-title":"IEEE Trans. Software Eng."},{"key":"6004_CR12","unstructured":"Churina, T.G. and Argirov, V.S., Modeling of Specifications of the SDL Language by Means of Modified HTT nets, Preprint of Ershov Inst. of Information Systems, Siberian Division, Russ. Acad. Sci., Novosibirsk, 2005, no. 124."},{"key":"6004_CR13","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/PCEE.2002.1115202","volume-title":"Proc. of Int. Conf. on Parallel Computing in Electrical Engineering","author":"V.E. Kozura","year":"2002","unstructured":"Kozura, V.E., Nepomniaschy, V.A., and Novikov, R.M., Verification of Distributed Systems Modeled by High-Level Petri Nets, Proc. of Int. Conf. on Parallel Computing in Electrical Engineering, Warsaw: IEEE Comput. Soc., 2002, pp. 61\u201366."},{"key":"6004_CR14","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D., Model Checking, MIT Press, 1999. Translated under the title Verifikatsiya modelei program: Model Checking, Moscow: MTsNMO, 2002."},{"key":"6004_CR15","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-540-40022-6_7","volume":"2472","author":"M. Weber","year":"2003","unstructured":"Weber, M. and Kindler, E., The Petri Net Markup Language, Petri Net Technology for Communication Based Systems, in Lecture Notes in Computer Science, 2003, vol. 2472, pp. 124\u2013144.","journal-title":"Lecture Notes in Computer Science"},{"issue":"11","key":"6004_CR16","doi-asserted-by":"publisher","first-page":"1616","DOI":"10.1109\/26.111443","volume":"39","author":"R. Cohen","year":"1991","unstructured":"Cohen, R. and Segall, A., An Efficient Reliable Ring Protocol, IEEE Trans. Commun., 1991, vol. 39, no. 11, pp. 1616\u20131624.","journal-title":"IEEE Trans. Commun."},{"key":"6004_CR17","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1016\/0169-7552(94)90045-0","volume":"26","author":"K. Imai","year":"1994","unstructured":"Imai, K., Ito, T., Kasahara, H., and Morita, N., ATMR: Asynchronous Transfer Mode Ring Protocol, Comput. Networks ISDN Systems, 1994, vol. 26, pp. 785\u2013798.","journal-title":"Comput. Networks ISDN Systems"},{"key":"6004_CR18","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49059-0_6","volume":"1579","author":"Y. Dong","year":"1999","unstructured":"Dong, Y. et al., Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools, in Lecture Notes in Computer Science (Proc. Int. Conf. TACAS\u201999), 1999, vol. 1579, pp. 74\u201388.","journal-title":"Lecture Notes in Computer Science (Proc. Int. Conf. TACAS\u201999)"},{"key":"6004_CR19","volume-title":"SDL with Applications from Protocol Specification","author":"B. Ferenc","year":"1991","unstructured":"Ferenc, B., Hogrefe, D., and Sarma, A., SDL with Applications from Protocol Specification, Englewood Cliffs: Prentice Hall, 1991."},{"key":"6004_CR20","doi-asserted-by":"crossref","unstructured":"Peng, H., Tahar, S., and Khendek, F., SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol, Proc. of the 3rd Int. Conf. on Formal Engineering Methods, IEEE Comput. Soc., 2000, pp. 79\u201387.","DOI":"10.1109\/ICFEM.2000.873808"},{"key":"6004_CR21","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-63166-6_8","volume":"1254","author":"R. Kaivola","year":"1997","unstructured":"Kaivola, R., Using Compositional Preorders in the Verification of Sliding Window Protocol, Lecture Notes in Computer Science, 1997, vol. 1254, pp. 48\u201359.","journal-title":"Lecture Notes in Computer Science"},{"key":"6004_CR22","doi-asserted-by":"crossref","unstructured":"Nepomniaschy, V.A., Alekseev, G.I., Bystrov, A.V., Mylnikov, S.P., Okunishnikova, E.V., Chubarev, P.A., and Churina, T.G., Verification of Estelle-Specified Communication Protocols Using High-Level Petri Nets, Programmirovanie, 2001, no. 2, pp. 5\u201320 [Programming Comput. Software (Engl. Transl.), 2001, vol. 27, no. 2, pp. 58\u201368].","DOI":"10.1023\/A:1011094609718"},{"issue":"10","key":"6004_CR23","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1109\/32.729680","volume":"24","author":"D.O. Keck","year":"1998","unstructured":"Keck, D.O. and Kuehn, P.J., The Feature and Service Interaction Problem in Telecommunications Systems: A Survey, IEEE Trans. Software Eng., 1998, vol. 24, no. 10, pp. 779\u2013796.","journal-title":"IEEE Trans. Software Eng."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768808060042.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768808060042","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768808060042","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768808060042.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:03:34Z","timestamp":1775009014000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768808060042"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11]]},"references-count":23,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,11]]}},"alternative-id":["6004"],"URL":"https:\/\/doi.org\/10.1134\/s0361768808060042","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11]]},"assertion":[{"value":"17 April 2008","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 November 2008","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}