Modeling of TCP Protocol in Event-B

Xue Jing Wang; Hong Zhang

doi:10.4028/www.scientific.net/AMM.263-266.1156

Paper Titles

An Approximate Formula for WER of TURBO-Like Codes over Fading Channels
p.1134

An Improved Design of the Carrier Communication Digital Multiplexer Implemented on Sports Venues
p.1138

An OFDM Channel Estimation Method with Radial Basis Function Neural Network
p.1142

Design and Realization of 10Gbps DPSK System for Free Space Optical Communication
p.1150

Modeling of TCP Protocol in Event-B
p.1156

On Performance of Combining Methods for Three-Node Relay Network
p.1160

Research of Rate-Matching for TD-SCDMA System
p.1165

Research on Realization of First Interleaving for TD-SCDMA System
p.1169

A New Dynamic Form Component Oriented GIS Applications
p.1173

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 263-266Modeling of TCP Protocol in Event-B

Modeling of TCP Protocol in Event-B

Abstract:

Event-B is a formal language for system modeling, which allows early-stage comparison of design alternatives and identifies potential sources of defects. Stop-and-Wait ARQ is the basis of data link layer protocols in TCP. Our work aims to model the protocol in Event-B to reduce development risks. The paper is presented in two parts: modeling of the error-free transmission in the protocol without time constraints, and then adding of time constraints to model the overtime retransmission.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 263-266)

Pages:

1156-1159

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.263-266.1156

Citation:

Cite this paper

Online since:

December 2012

Authors:

Xue Jing Wang, Hong Zhang

Keywords:

Event-B, Modeling, TCP

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] Mohammad Reza Sarshogh, Michael Butler, Specification and refinement of discrete timing properties in Event-B, AVoCS2011.Volume 36

Google Scholar

[2] Information on http://en.wikipedia.org/wiki

Google Scholar

[3] Woodside, C.M. Performance Petri net analysis of communications protocol software by delay-equivalent aggregation. Petri Nets and Performance Models. (PNPM91). Pp64-73. (1991)

DOI: 10.1109/pnpm.1991.238781

Google Scholar

[4] Bochmann, G. Formal Methods in Communication Protocol Design. IEEE Transactions on Communications. Volume 28. Pp624-631. April (1980)

DOI: 10.1109/tcom.1980.1094685

Google Scholar

[5] J-R. Abrial, M. J. Butler, S. Hallerstede, T.S. Hoang, F.Mehta, L.Voisin. Rodin: an open toolset for modeling and reasoning in Event-B. STTT 12(6):447-466, (2010)

DOI: 10.1007/s10009-010-0145-y

Google Scholar

[6] J-R. Abrial, M. J. Butler, S. Hallerstede, L. Voisin. An Open Extensible Tool Environment for Event-B. In ICFEM. Pp. 588-605(2006)

DOI: 10.1007/11901433_32

Google Scholar

[7] M.J. Butler, J. Falampin. An Approach to Modelling and Refining the Timing Properties in B. In Refinement of Critical Systems (RCS). January (2002)

Google Scholar