Suleiman Sadiq MSc Dissertation 2012/13

Data Communications and Protocol Verification

Supervised by M.Gheorghe

Abstract

For distributed systems to communicate effectively with high assurance, reliability engineers standardize on network protocols that are required to function with high performance at any given time. The consequence of unexpected behaviors in such communication protocols can result in decreased network performance, security breaches or even complete network break down. For this reason, protocols must be completely checked for specification or implementation errors. Traditional testing does not scale due to the exponential increase in the state space of these communication protocols. Formal and thorough verification techniques are often classified as difficult and highly impractical due to the complexity of their specification languages, and are therefore rarely used in checking correctness of network protocols.

            In this research, current formal verification methodologies are first investigated. The scope is then limited to model checking which is experimented by specification and verification of the classic Alternating Bit Protocol (ABP), widely used File Transfer Protocol (FTP), well-known Sliding Window (SW) Protocol and the more complex GIGAMAX Cache Coherence Protocol. The protocols are modeled using the description languages of NuSMV and SPIN model checkers. Properties are described in Computation Tree Logic and Linear Temporal Logic, and verification performed using NuSMV and SPIN model checkers.

            A common problem in the application and usability of formal verification techniques is how to make the formalism intuitive while preserving its effectiveness. This thesis further introduces Temporal Logic Specification Tool (TLogicSpec), a tool that aims to address this problem. The tool provides a medium for formulating temporal logic properties from a template of well formulated, correct and pre-verified properties. The tool also considers automatic translation of properties described in natural language to temporal logic. A functional prototype of this tool is implemented in java.