Title:

Computer Communications and Interfacing

Code:KPA
Ac.Year:ukončen 2003/2004
Term:Winter
Study plans:
ProgramBranchYearDuty
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:6
Completion:examination (written)
Type of
instruction:
Hour/semLecturesSem. ExercisesLab. exercisesComp. exercisesOther
Hours:39001214
 ExaminationTestsExercisesLaboratoriesOther
Points:60150025
Guarantee:Švéda Miroslav, prof. Ing., CSc., DIFS
Lecturer:Švéda Miroslav, prof. Ing., CSc., DIFS
Instructor:Bureš František, Ing., DIFS
Matoušek Petr, Ing., Ph.D., DIFS
Očenášek Pavel, Ing., Ph.D., DIFS
Ryšavý Ondřej, Ing., Ph.D., DIFS
Strach Michal, Ing., 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.
Learning outcomes and competences:
Understanding basic concepts and principles of formal specifications of reactive systems and real-time systems.
Syllabus of lectures:
  1. Introduction, real-time systems.
  2. Introduction to Temporal logic.
  3. Formal specifications and model checkers.
  4. Temporal Logic.
  5. Time models, Liveness, safety, fairness. Real-time liveness.
  6. Temporal logic and real time.
  7. Test
  8. Fieldbus protocols.
  9. Formal specifications and provers.
  10. Case study - Internet and real-time applications.
  11. Case Study - Designing distributed applications.
  12. Exam
Syllabus of computer exercises:
  1. Temporal logics LTL, CTL, theorem proving
  2. Introduction to SPIN
  3. Model checking (SPIN, SMV)
  4. Using SPIN to protocol verification
  5. An overview of formal tools
  6. Communication to embedded devices
Syllabus - others, projects and individual work of students:
  1. A reactive system modeling in Spin
  2. A report on new aproaches in the area of formal specification and verification
Fundamental literature:
  1. de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
Study literature:
  1. 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 projects in due dates