Course details

Computer Communications and Interfacing

KPA Acad. year 2006/2007 Summer semester 5 credits

Current academic year

Course is not open in this year
Real-time distributed systems. Models for discrete-event and real-time systems. Temporal logics. Formal specifications and verification. Model checking. Real-time systems verification. Real-time protocols. Applications design.


Language of instruction



Examination (written)

Time span

39 hrs lectures, 2 hrs laboratories, 4 hrs pc labs, 7 hrs projects

Assessment points

60 exam, 15 half-term test, 25 projects




Subject specific learning outcomes and competences

Understanding basic concepts and principles of formal specifications of reactive systems and real-time systems.

Learning objectives

Be informed about formal specification principles aimed at reactive systems and real-time systems modeling; be aware of real-time communication protocols.


Prerequisite kwnowledge and skills

Propositional logic. Basics of the first-order logic. The elementary notions of communication protocols.

Study literature

  • de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.

Fundamental literature

  • de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.

Syllabus of lectures

  • Introduction.
  • Distributed systems design principles.
  • Real-time distributed systems.
  • Models for discrete-event systems and real-time systems.
  • Liveness, safety, fairness. Real-time liveness.
  • Introduction to temporal logics.
  • Temporal logic and real time.
  • Formal specifications and provers.
  • Formal specifications and model checkers.
  • Fieldbus protocols.
  • Internet and real-time applications.
  • Designing distributed applications.
  • Case studies.

Syllabus of computer exercises

  • Spin and Promela
  • Algorithm simulaion in Spin
  • Model checking
  • Fieldbus-level protocols
  • CANalyzer
  • Intranet and CANalyzer

Syllabus - others, projects and individual work of students

  • A reactive system modeling in Spin
  • Analysis of a Fieldbus-level protocol

Progress assessment

Written mid-term exam and submitting 2 projets in due dates

Controlled instruction

Completion of 2 projects, mid-term exam passing

Course inclusion in study plans

  • Programme EI-MSC-3, field VTN, 3rd year of study, Elective
  • Programme EI-MSC-5, field VTI, 5th year of study, Elective
Back to top