This thesis addresses the analysis of communication protocols in distributed systems, where increasing system complexity makes manual analysis unreliable. The objective of the thesis is to develop a software tool that enables formal specification of protocols and their automatic analysis using the Perturbation of Global System States (PGSS) method. Protocols are modeled using deterministic finite automata, while the analysis is based on a systematic exploration of the global state space. The developed tool provides a clear graphical representation of reachable states and transitions, as well as the detection of common errors such as deadlocks, full queues, and undefined message receptions. The correctness of the tool is validated using the Alternating Bit Protocol, with the results confirming both the correctness of the implementation and the practical usefulness of the proposed approach.
|
