Faculty of Information Technology, BUT

Course details

Computer Communications and Interfacing

KPA Acad. year 2004/2005 Winter semester 6 credits

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.

Guarantor

Language of instruction

Czech

Completion

Examination (written)

Time span

39 hrs lectures, 12 hrs pc labs, 14 hrs projects

Assessment points

60 exam, 15 half-term test, 25 projects

Department

Lecturer

Instructor

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.

Prerequisites

Study literature

  • Huth M.R.A., Ryan M.D.: Logic in Computer Science. Cambridge University Press, 2002.

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 - 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 projects in due dates

Controlled instruction

Completion of 2 projects, mid-term exam passing
Back to top