Course details
Computer Communications and Interfacing
KPA Acad. year 2006/2007 Summer semester 5 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
Completion
Time span
- 39 hrs lectures
- 2 hrs laboratories
- 4 hrs pc labs
- 7 hrs projects
Department
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 knowledge 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
Progress assessment
Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.
Controlled instruction
Completion of 2 projects, mid-term exam passing