Communication protocols

Course guarantor:

Jan Janeček

Lecturer:

Tutor:

Jan Janeček

Supervisor:

Department of Computer Systems

Synopsis:

Students will learn the trends of modern communication protocols development, architectures of selected distributed systems, and formal tools for their specification, modeling and verification.

Requirements:

Syllabus of lectures:

1.Principles of modern communication protocols.

2.Automata description of protocols, application of verification methods for distributed mechanisms.

3.Exploitation of attributed grammars, the RTAG system.

4.Promela and ESTELLE prototype systems.

5.SPIN system based on the Promela process.

6.The LOTOS specification language.

7.Validation and verification algorithms.

8.Extension of SPIN for model checking.

9.Transformations of protocols.

10.Dynamic behavior of protocols in heavily loaded networks.

Syllabus of tutorials:

Study Objective:

Fault-protection mechanisms for communication protocols have lead to construction of verification and tolerance systems. Recently they are closed to implementation of verification mechanisms for distributed applications and their robustness and resistance. The aim of the module is to introduce students into the context of the modern communication protocols development.

Study materials:

1.Holzmann G.J.: Design and Validation of Computer Protocols. Prentice Hall 1998

2.Ben-Ari M.: Principles of the SPIN Model Checker, Springer 2008.

Note:

Time-table for winter semester 2024/2025:

Time-table is not available yet

Time-table for summer semester 2024/2025:

Time-table is not available yet

The course is a part of the following study plans:

• Informatics (doctoral) (compulsory elective course)
• Informatics (compulsory elective course)