Formal Specification and Verification of Transmission Control Protocol
Abdessamad Jarrar, Otman Bellasri, Sallami Chougdali, Youssef Balouki · 2017
As computer networks proliferate, the design of properly functioning communication procedures or protocols becomes ever more important. Protocols define the set of rules needed to exchange messages between communicating entities even if these communication protocols are often touted as being robust. Yet they had revealed through their use inconsistencies, ambiguities, and incompleteness that cannot go undetected. Since such systems are often deployed in safety-critical applications, confidence in protocol correctness is highly required. One way of achieving this goal is by using formal methods that can have an impact in increasing our understanding of such systems. This study provides a model to use on any communication protocol (CP) using formal methods by transforming all the requirements and events of CP to mathematical approach, integrating all the techniques of fault avoidance that help in the reduction of errors introduced into a system. There are a lot of formal methods; we conduct our concentration to Event B method.