Courses Currently Offered in English

Course Version

Course Code:EADCP
Version Number:1
Course Name:Analisys and Design of Communications Protocols
Credit Units:4
ECTS:6
Cost Units:30
Examination type (E-with exam):E
Grading threshold:5
Initiation semester:03L
Person responsible:dr inż. Krzysztof Brzeziński
Description:ICT programme taught in English

Hours per week

Class typeHours
W2
P2

Class types: W - lecture, C - tutorial, L - laboratory, P - project

Prerequisites

---

Prerequitise types: W - required, Z - recommended

Similar Courses

---

Last Course Instances

Semester codeInstance codeLecturerInstituteMax. number of students
07LAdr inż. Krzysztof BrzezińskiTK30

Thematic Classification

Class CodeClass name (in Polish)
ANGLAll Courses in English (A)

Conspectus

Summary (in Polish)

Przedmiot dotyczy jednego z podstawowych zagadnień w dziedzinie telekomunikacji, jakim jest projektowanie, implementacja i weryfikowanie protokołów telekomunikacyjnych. W odróżnieniu od innych dziedzin (jak np. teoria kolejek), w których nacisk został położony na zjawiska o charakterze ilościowym, przedmiot niniejszy koncentruje się na poprawności logicznej i metodach jej uzyskania zarówno w teorii, jak i w praktyce telekomunikacyjnej. Jako podstawę dla rozważań wprowadza się specyficzny aparat formalny, pokrewny teorii grafów / automatów / procesów.

Lecture contents

Introduction. History of research on protocols. Characteristics, correctness criteria and generic design problems of communications systems. The idea of a protocol (Merlin) (2h).

Protocol life-cycle, "point of discontinuity". Generic and specific properties of a protocol. Approaches to protocol life-cycle (2h).

Specification vs description. Languages and formalisms: SDL, Estelle, Lotos, MSC, ASN.1+BER, TTCN. Semantic base: temporal logics, process algebrae, automata-based approach. Use of temporal logic for stating protocol properties (2h).

Detailed discussion of automata-based model. Global automaton vs automata of individual agents. Specification styles. Formalization: FSM, EFSM. Zafiropulo notation. System model: CFSM. Models of communication channels. Global state: definable vs reachable. System behaviour: interleaving, trace. Reachable state space and its representation. Error models (3h).

Constructing a reachability graph. Quality and coverage of exploration. Exploration: full (exhaustive), partial, random walk. Algorithms for partial exploration: Holzmann - supertrace, bitstate hashing. Multihash: parallel, serial. Reduced reachability (Cacciari) (4h).

MSC language. Partial vs total order. Basic elements of the language. Behaviour "consistent with" a MSC chart (2h).

A protocol in a layered communication architecture: abstract model and implementation issues. Structure of static information elements (messages): tabular specification, ASN.1, coding rules (BER) (2h).

Verification of the implementation. Passive vs active testing. Conformance vs interoperability testing. Models based on implementation and conformance relations. Industrial setting for conformance testing - ISO 9646. Protocol properties in international standards: PICS documents. Static and dynamic conformance. Formulating requirements for implementations (2h).

Conformance testing: implementation under test, testing architectures, testing context, structure of a single test and a test suite. TTCN2 language - constructs, semantics, and use cases. Standardized testing process. Information on TTCN3 (4h).

Automatic generation of conformance tests from FSM specifications: DS, W, E, UIO methods. Other types of tests. Theory and applications of passive testing (3h).

Recapitulation (2h).

Project contents

Students solve, in small groups, design or analytical projects chosen from a fixed set of projects (a particular project proposed by a group may be considered). Examples of projects: to design and implement a simplified system for the automatic verification of protocols; to specify and check properties of a well known protocol (e.g. leader election or eating philosophers); to design and implement an "oracle" that decides whether a given trace is consistent with a partially specified behaviour.

References
  1. G.J.Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1991
  2. K.M.Brzeziński, Testing of protocol implementations. Copy of presentation slides.
  3. K.M.Brzeziński, Introduction to the theory and practice of protocol testing. Script
  4. selected conference papers indicated by the lecturer.
Summary

The course covers one of the most fundamental issues in telecommunications, which is the design, implementation and verification of communication protocols. Protocol science (or interaction science) discusses such issues in the context of logical correctness of both an abstract, mathematical object (protocol under design) and its incarnation in a real hardware/software piece of equipment. It is worth noting that many other branches of science, such as e.g. queueing theory, focus rather on quantitative, stochastic, time-related correctness criteria. During the course a particular set of formal means of expression will be used, akin to automata theory, graph theory and process theory.