Abstract
For modeling, specification and verification of telecommunication systems, the models such as finite automata, Petri nets and their generalizations are usually applied. The goal of our paper is to represent a new two-level approach for modeling, specification and verification of telecommunication systems. On the first level, telecommunication systems are specified by communicating extended finite automata, while on the second level the automata systems are translated into coloured Petri nets (CPN). Correctness of the translation algorithm is justified by proving bisimilarity between the resulting CPN and the automata system. This method is applied to investigation of two case studies: ring protocols (RE-protocol and ATMR-protocol) and the feature interaction problem in telephone networks. CPN Tools [9] are used for modeling these telecommunication systems and constructing reachability graphs of CPN. We used the Petri Net Verifier [11] for verification of the net models with respect to properties expressed in mu-calculus by the model checking method.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Calder, M., Miller, A.: Using SPIN for Feature Interaction Analysis – A Case Study. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 143–162. Springer, Heidelberg (2001)
Capellmann, C., Dibold, H., Herzog, U.: Using High-Level Petri Nets in the Field of Intelligent Networks. In: Billington, J., Díaz, M., Rozenberg, G. (eds.) APN 1999. LNCS, vol. 1605, pp. 1–36. Springer, Heidelberg (1999)
Cavalli, A., Maag, S.: A New Algorithm for Service Interaction Detection. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 371–382. Springer, Heidelberg (2002)
Cohen, R., Segall, A.: An Efficient Reliable Ring Protocol. IEEE Transactions on Communications 39(11), 1616–1623 (1991)
Gibson, P., Hamilton, G., Mery, D.: Integration Problems in Telephone Feature Requirements. In: Proc. of the 1st Intern. Conf. on Integrated Formal Methods, York (IFM 1999), pp. 129–148. Springer, Heidelberg (1999)
Guelev, D., Ryan, M., Schobbens, Yv.: Model-checking the Preservation of Temporal Properties upon Feature Integration. Int. J. on Software Tools for Technology Transfer 9(1), 53–62 (2007)
Imai, K., Ito, T., Kasahara, H., Morita, N.: ATMR: Asynchronous transfer mode ring protocol. Computer Networks and ISDN Systems 26, 785–798 (1994)
Jensen, K.: Coloured Petri Nets: basic concepts, analysis methods and practical use, vol. 1, 2, 3. Springer, Heidelberg (1996)
Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for modeling and validation of concurrent systems. Int. J. on Software Tools for Technology Transfer 9, 213–254 (2007)
Keck, D.O., Kuehn, P.J.: The Feature and Service Interaction Problem in Telecommunications Systems: A Survey. IEEE Trans. on Software Eng. 24(10), 779–796 (1998)
Kozura, V.E., Nepomniaschy, V.A., Novikov, R.M.: Verification of Distributed Systems Modelled by High-level Petri Nets. In: Proc. Intern. Conf. on Parallel Computing in Electrical Engineering, Warsaw, Poland, pp. 61–66. IEEE Comp. Society, Los Alamitos (2002)
Lee, D.: Principles and methods of testing finite state machines. Proc. IEEE 84(8), 1090–1123 (1996)
Lorentsen, L., Tuovinen, A., Xu, J.: Modelling Feature Interaction Patterns in Nokia Mobile Phones using Coloured Petri Nets and Design/CPN. In: Proc. 3rd Workshop on Practical Use of Coloured Petri Nets (CPN 2001), Aarhus Univ., DAIMI PB-554, pp. 1–14 (2001)
Nakamura, M.: Design and Evaluation of Efficient Algorithms for Feature Interaction Detection in Telecommunication Services. PhD dissertation, Osaka University (1999)
Nepomniaschy, V., Beloglazov, D., Churina, T., Mashukov, M.: Using Coloured Petri Nets to Model and Verify Telecommunications Systems. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) Computer Science – Theory and Applications. LNCS, vol. 5010, pp. 360–371. Springer, Heidelberg (2008)
Peng, H., Tahar, S., Khendek, F.: SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol. Int. J. on Software Tools for Technology Transfer 4(2), 234–248 (2003)
Schatz, B., Salzmann, C.: Service-based systems engineering: Consistent combination of services. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 86–104. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beloglazov, D., Nepomniaschy, V. (2010). A Two-Level Approach for Modeling and Verification of Telecommunication Systems. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2009. Lecture Notes in Computer Science, vol 5947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11486-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-11486-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11485-4
Online ISBN: 978-3-642-11486-1
eBook Packages: Computer ScienceComputer Science (R0)