Modelling Communication Protocols

Master thesis, offered

University: MU, Faculty: FI, Topic: Distributed Systems

Automatic verification of unmodified code is presently not mature enough to handle industry-level software. Instead the student will manually create models of various protocols used by Y Soft SafeQ for distributed communication. It will be possible to demonstrate that these models are specifications of their SafeQ implementations. The student will then formulate a given set of requirements for each protocol in a temporal logic and prove the models to satisfy their requirements using the DIVINE model checker.

Thesis detail is available on

YSoft SAFEQ Breeze Beta
YSoft SAFEQ Breeze Beta

SMB can now lose the IT hassle of supporting print services.