Verification of Design Decisions in Communication Protocol by Evaluation of Temporal Logic Formulas

TL;DR

This paper demonstrates how formal specification and temporal logic verification can be used to validate design decisions in communication protocols, ensuring correctness during development.

Contribution

It presents a case study of verifying communication protocol design decisions using CSM automata and temporal logic, illustrating the practical application of formal methods.

Findings

Verification confirms correctness of design decisions

Formal methods effectively identify potential issues

Temporal logic provides precise specification

Abstract

During the project of a communication protocol, many design decisions influence the behavior of the protocol and its correctness. Formal specification and verification of the protocol may prove its correctness. In this paper, an example of a verification of design decision using formal specification in CSM automata and verification in temporal logic is presented.