Title:

Computer Communications and Interfacing

Code:KPA
Ac.Year:ukončen 2005/2006
Term:Summer
Curriculums:
ProgrammeBranchYearDuty
EI-BC-3VTB2nd Stage/2nd YearElective
EI-MSC-3VTN3rdElective
EI-MSC-5VTI2nd Stage/3rd YearElective
Language:Czech
Private info:http://www.fit.vutbr.cz/study/courses/KPA/private/
Credits:5
Completion:examination (written)
Type of
instruction:
Hour/semLecturesSem. ExercisesLab. exercisesComp. exercisesOther
Hours:390247
 ExaminationTestsExercisesLaboratoriesOther
Points:60150025
Guarantee:Švéda Miroslav, prof. Ing., CSc., DIFS
Lecturer:Švéda Miroslav, prof. Ing., CSc., DIFS
Instructor:Ryšavý Ondřej, doc. Ing., Ph.D., DIFS
Ščuglík František, Ing., Ph.D., DIFS
Faculty:Faculty of Information Technology BUT
Department:Department of Information Systems FIT BUT
Prerequisites: 
Data Communications and Computer Networks (PDT), DIFS
 
Learning objectives:
  Be informed about formal specification principles aimed at reactive systems and real-time systems modeling; be aware of real-time communication protocols.
Description:
  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.
Knowledge and skills required for the course:
  Propositional logic. Basics of the first-order logic. The elementary notions of communication protocols.
Learning outcomes and competences:
  Understanding basic concepts and principles of formal specifications of reactive systems and real-time systems.
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
Fundamental literature:
 
  • de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
Study literature:
 
  • de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
Controlled instruction:
  Completion of 2 projects, mid-term exam passing
Progress assessment:
  Written mid-term exam and submitting 2 projets in due dates