Verification of Design Decisions in Communication Protocol by Evaluation of Temporal Logic Formulas
This work addresses correctness verification for communication protocol designers, but it appears incremental as it applies existing methods without new breakthroughs.
The paper tackled the problem of verifying design decisions in communication protocols by presenting an example using formal specification with CSM automata and verification via temporal logic, but it did not provide concrete results or numbers.
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.