| Peer-Reviewed

Verification of Telecommunication Protocols Based on Formal Methods

Published: 20 February 2013
Views:       Downloads:
Abstract

This article is devoted to the development method for verification and detecting errors that can occur in the operation of protocols for information exchange. The various steps of verification of telecommunication protocols are given in the article; the construction of counterexample, which helps to identify the logical operations that lead to errors in the protocols. Practical implementation of given method is shown on TCP.

Published in International Journal of Intelligent Information Systems (Volume 2, Issue 1)
DOI 10.11648/j.ijiis.20130201.11
Page(s) 1-10
Creative Commons

This is an Open Access article, distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution and reproduction in any medium or format, provided the original work is properly cited.

Copyright

Copyright © The Author(s), 2013. Published by Science Publishing Group

Keywords

Verification, Model Checking, E-nets, Formal Grammars, Implementation Model, Specification Model

References
[1] ISO/IEC 14102:2008. Information technology - Guideline for the evaluation and selection of CASE Tools, 2008.
[2] The Standish Group. The Scope of Software Development Project Failures: The Standish Group. Stanford, 2009, http://www.cs.nmt.edu/~cs328/reading/Standish.pdf.
[3] Jr. Clarke, M. Edmund, and A. Peled, Model Checking, MIT Press, 1999, ISBN 0-262-03270-8.
[4] B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and P. Schnoebelen, Systems and Software Verification: Model-Checking Techniques and Tools, 2009. ISBN 3-540-41523-8
[5] C. P. Stirling, "Modal and temporal logics for processes". LNCS 1043, 1996, pp. 149–237.
[6] J. Bradfield, C. Stirling, "Modal logics and mu-calculi", Inf.ed.ac.uk
[7] G Nutt, "Evaluation Nets for Computer Systems Performance Analysis". FJCC, AFIPSPRESS. 1972, pp. 279 – 286.
[8] A. Mironov, "A new method of verification of protocols of data transmission through unreliable medium", Summer School in Software Engineering and Verification, Moscow, 2011, pp. 261 –276.
[9] N. Chomsky, "Three Models for the Description of Language". IRE Transactions on Information Theory 2 (2). 1956, pp. 113–123. doi:10.1109/TIT.1956.1056813.
[10] E. Korovchenko, "Models and methods for analysis and verification telecommunications protocols based on the E-networks and formal grammars", Master’s thesis, Kharkov national University of Radio electronics, Oct. 2011.
[11] E. Duravkin, E. Korovchenko, "The formalization of the information exchange protocols behavior provided by models based on E-network", the problems of telecommunication (e-journal). vol. 1 (3). pp. 28 – 38, 2011: http://pt.journal.kh.ua/2011/1/1/111_duravkin_verification.pdf.
[12] A.T.S. Abu-Jassar, O. Tkachova, "Patterns for reliable Web-services", The problems of telecommunication (e-journal). vol. 2 (7), pp. 36–42, 2012: http://pt.journal.kh.ua/2012/2/1/122_tkachova_web.pdf.
[13] L. Hoffman, "Talking Model-Checking Technology", Communications of the ACM, 2008, pp. 110–112.
[14] Formal Grammar: 14th International Conference, FG 2009, Bordeaux, France, July 25-26, 2009.
[15] J. Postel, Transmission control protocol. RFC 793, California, sept. 1981, 85 p.
[16] A. Strunk An algorithm to predict the QoS-Reliability of service compositions. In: SERVICES, 2010, pp. 205–212.
Cite This Article
  • APA Style

    Tkacheva Elena Borisovna, Lubov Demchenko Vasilievna, Saied Halawa Fawaz. (2013). Verification of Telecommunication Protocols Based on Formal Methods. International Journal of Intelligent Information Systems, 2(1), 1-10. https://doi.org/10.11648/j.ijiis.20130201.11

    Copy | Download

    ACS Style

    Tkacheva Elena Borisovna; Lubov Demchenko Vasilievna; Saied Halawa Fawaz. Verification of Telecommunication Protocols Based on Formal Methods. Int. J. Intell. Inf. Syst. 2013, 2(1), 1-10. doi: 10.11648/j.ijiis.20130201.11

    Copy | Download

    AMA Style

    Tkacheva Elena Borisovna, Lubov Demchenko Vasilievna, Saied Halawa Fawaz. Verification of Telecommunication Protocols Based on Formal Methods. Int J Intell Inf Syst. 2013;2(1):1-10. doi: 10.11648/j.ijiis.20130201.11

    Copy | Download

  • @article{10.11648/j.ijiis.20130201.11,
      author = {Tkacheva Elena Borisovna and Lubov Demchenko Vasilievna and Saied Halawa Fawaz},
      title = {Verification of Telecommunication Protocols Based on Formal Methods},
      journal = {International Journal of Intelligent Information Systems},
      volume = {2},
      number = {1},
      pages = {1-10},
      doi = {10.11648/j.ijiis.20130201.11},
      url = {https://doi.org/10.11648/j.ijiis.20130201.11},
      eprint = {https://article.sciencepublishinggroup.com/pdf/10.11648.j.ijiis.20130201.11},
      abstract = {This article is devoted to the development method for verification and detecting errors that can occur in the operation of protocols for information exchange. The various steps of verification of telecommunication protocols are given in the article; the construction of counterexample, which helps to identify the logical operations that lead to errors in the protocols. Practical implementation of given method is shown on TCP.},
     year = {2013}
    }
    

    Copy | Download

  • TY  - JOUR
    T1  - Verification of Telecommunication Protocols Based on Formal Methods
    AU  - Tkacheva Elena Borisovna
    AU  - Lubov Demchenko Vasilievna
    AU  - Saied Halawa Fawaz
    Y1  - 2013/02/20
    PY  - 2013
    N1  - https://doi.org/10.11648/j.ijiis.20130201.11
    DO  - 10.11648/j.ijiis.20130201.11
    T2  - International Journal of Intelligent Information Systems
    JF  - International Journal of Intelligent Information Systems
    JO  - International Journal of Intelligent Information Systems
    SP  - 1
    EP  - 10
    PB  - Science Publishing Group
    SN  - 2328-7683
    UR  - https://doi.org/10.11648/j.ijiis.20130201.11
    AB  - This article is devoted to the development method for verification and detecting errors that can occur in the operation of protocols for information exchange. The various steps of verification of telecommunication protocols are given in the article; the construction of counterexample, which helps to identify the logical operations that lead to errors in the protocols. Practical implementation of given method is shown on TCP.
    VL  - 2
    IS  - 1
    ER  - 

    Copy | Download

Author Information
  • Kharkiv National University of Radio and Electronics, Kharkov, Ukraine

  • Kharkiv National University of Radio and Electronics, Kharkov, Ukraine

  • Kharkiv National University of Radio and Electronics, Kharkov, Ukraine

  • Sections