Verification of Telecommunication Protocols Based on Formal Methods

Tkacheva Elena Borisovna; Lubov Demchenko Vasilievna; Saied Halawa Fawaz

doi:doi:10.11648/j.ijiis.20130201.11

| Peer-Reviewed

Verification of Telecommunication Protocols Based on Formal Methods

Tkacheva Elena Borisovna, Lubov Demchenko Vasilievna, Saied Halawa Fawaz

Published in International Journal of Intelligent Information Systems (Volume 2, Issue 1)

Published: 20 February 2013

Views: Downloads:

Download PDF

Share This Article

Twitter
Linked In
Facebook

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

Plain Text BibTeX RIS

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

Tkacheva Elena Borisovna

Kharkiv National University of Radio and Electronics, Kharkov, Ukraine
Lubov Demchenko Vasilievna

Kharkiv National University of Radio and Electronics, Kharkov, Ukraine
Saied Halawa Fawaz

Kharkiv National University of Radio and Electronics, Kharkov, Ukraine

Download PDF

Sections

Plain Text BibTeX RIS

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