Abstract
Estelle specifications are considered that include certain dynamic constructs. A method of translation of these specifications into modified colored Petri nets is described. Static Estelle specifications are translated into hierarchical typed time nets (HTT nets), which are extensions of safe colored Petri nets through the introduction of the notions of time, priorities, and places (which are queues of tokens). A program complex EPV is presented that is designed for verification of static Estelle specifications of communication protocols by translating them into HTT nets. Experiments are described on simulation and search for semantic errors in protocols used in practice.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.REFERENCES
Alekseev, G.I., Bystrov, A.V., Kurtov, S.A., et al., Use of Petri Nets for Verification of Estelle-Represented Distributed Systems, Izv. Ross. Akad. Nauk, Teor. Sist. Upr., 1999, no. 5, pp. 105-116.
Zaitsev, S.S., Opisanie i realizatsiya protokolov setei EVM (Description and Implementation of Computer Communication Protocols), Moscow: Nauka, 1989.
Kotov, V.E., Seti Petri (Petri Nets), Moscow: Nauka, 1984.
Nepomniaschy, V.A. et al., Verifikatsiya Estelle-spetsi-fikatsii raspredelennykh sistem posredstvom raskrashennykh setei Petri (Verification of Estelle Specifications of Distributed Systems by Means of Colored Petri Nets), Novosibirsk, 1998.
Okunishnikova, E.V., Modeling of Dynamic Estelle Constructs by Means of Colored Petri Nets, Preprint of Ershov Inst. of Information Systems, Siberian Division, Russ. Acad. Sci., Novosibirsk, 2000, no. 78.
Alekseev, G.I. et al., Petri-Net Based Environment for the Specification, Analysis and Simulation of Concurrent Systems, in Specification, Verification and Net Models of Concurrent Systems, Novosibirsk, 1994, pp. 116-127.
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-273.
Bucci, G. and Vicario, E., Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets, IEEE Trans. Software Eng., 1995, vol. 21, no. 12, pp. 969-991.
Budkowski, S. and Dembinski, P., An Introduction to Estelle: A Specification Language for Distributed Systems, Comput. Networks ISDN Systems, 1988, vol. 14, no. 1, pp. 3-23.
Churina, T.G. and Okunishnikova, E.V., Coloured Petri Nets Approach to the Validation of Estelle Specifications, Proc. of Workshop on Concurrency, Specification and Programming, Warsaw, Poland, 1997, pp. 25-36.
Cohen, R. and Segall, A., An Efficient Reliable Ring Protocol, IEEE Trans. Commun., 1991, vol. 39, no. 11, pp. 1616-1624.
Dembinski, P., http://www.ipipan.waw.pl/piotrd/estellespec/ abra_prot.stl.
Dimitrov, V. and Petkov, A., Verification Oriented Estelle Specification of Communication Protocols, in Research into Networks and Distributed Applications, Amsterdam: North-Holland, 1988, pp. 953-960.
Dong, Y. et al., Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools, Proc. Int. Conf. TACAS'99, Lecture Notes in Computer Science, vol. 1579, Berlin: Springer, 1999, pp. 74-88.
Ferenc, B., Hogrefe, D., and Sarma, A., SDL with Applications from Protocol Specification, Englewood Cliffs: Prentice Hall, 1991.
Fisher, J. and Dimitrov, E., Verification of SDL'92 Specifications Using Extended Petri Nets, Proc. IFIP Fifteenth Int. Conf. on Protocol Specification, Testing and Verification, Warsaw, 1995, pp. 455-458.
Information Processing Systems-Open Systems Interaction-ESTELLE: A Formal Description Technique Based on an Extended State Transition Model: International Standard, 1989, ISO 9074.
Jensen, K., Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 1: Basic Concepts, Berlin: Springer, 1996.
Jensen, K., Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 2: Analysis Methods, Berlin: Springer, 1996.
Jensen, K., Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 3: Practical Use, Berlin: Springer, 1997.
Kaivola, R., Using Compositional Preorders in the Veri-fication of Sliding Window Protocol, Lecture Notes in Computer Science, vol. 1254, Berlin: Springer, 1997, pp. 48-59.
Kristensen, L.M., Christensen, S., and Jensen, K., The Practitioner's Guide to Coloured Petri Nets, Int. J. Software Tools Techn. Transfer, 1998, vol. 2, no. 2, pp. 98-132.
Lai, R. and Jirachiefpattana, A., Verifying Estelle Protocol Specifications Using Numerical Petri Nets, Comput. Syst. Sci. Eng., 1996, vol. 11, no. 1, pp. 15-33.
Nepomniaschy, V.A. et al., Petri Net Modelling of Estelle-Specified Communication Protocols, Proc. 3rd Int. Conf. Parallel Computing Technologies, Lecture Notes in Computer Science, vol. 964, Berlin: Springer, 1995, pp. 94-108.
Nepomniaschy, V.A. et al., EPV-Petri Net Based Estelle Protocol Verifier, Proc. 1st Int. Workshop on the Formal Description Technique Estelle, Evry, France, 1998, pp. 101-108.
Richier, J.L., Rodriguez, C., Sifakis, J., and Voiron, J., Verification in XESAR of the Sliding Window Protocol, Proc. 7th IFIP Int. Symp. on Protocol Specification, Testing and Verification, 1987, pp. 235-248.
Stenning, N.V., A Data Transfer Protocol, Comput. Networks, 1976, vol. 1, no. 2, pp. 99-110.
Tsang, T. and Lai, R., Specification and Verification of Multimedia Synchronization Scenarios Using Time-Estelle, Software Practice Experience, 1998, vol. 28, no. 11, pp. 1185-1211.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Nepomniaschy, V.A., Alekseev, G.I., Bystrov, A.V. et al. Verification of Estelle-Specified Communication Protocols Using High-Level Petri Nets. Programming and Computer Software 27, 58–68 (2001). https://doi.org/10.1023/A:1011094609718
Issue Date:
DOI: https://doi.org/10.1023/A:1011094609718