Faculty of Information Technology, BUT

Course details

Specification of Embedded Systems

SVD Acad. year 2001/2002 Winter semester

Embedded distributed system design principles. Reactive systems and real-time systems. Reactive system and real-time system models. Fairness, livness, safety, feasibility; real-time livness. Temporal logic fundamentals. Time models and temporal logics. Temporal logic and real time. Formal specifications of embedded systems. Hybrid systems. Provers. Model checking. Real-time systems verification. Fieldbus-type protocols. Internet and embedded systems.

Guarantor

Language of instruction

Czech

Completion

Examination (oral)

Time span

39 hrs lectures

Assessment points

Lecturer

Subject specific learning outcomes and competences

Understanding formal specification principles as applied to embedded systems design; be aware of utilizing temporal logics for modeling reactive systems and real-time systems; being informed about embedded distributed system architectures.

Learning objectives

Understand formal specification principles as applied to embedded systems design; be aware of utilizing temporal logics for modeling reactive systems and real-time systems; be aware of embedded distributed system architectures.

Study literature

  • Alur R., Henzinger T.A. (Editors): Hybrid Systems III - Verification and Control. Springer-Verlag, LNCS 1066, 1996.
  • de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
  • Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.

Fundamental literature

  • Alur R., Henzinger T.A. (Editors): Hybrid Systems III - Verification and Control. Springer-Verlag, LNCS 1066, 1996.
  • de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
  • Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.

Syllabus of lectures

  • Embedded distributed system design principles
  • Reactive system and real-time system models
  • Fairness, livness, safety, feasibility; real-time livness
  • Temporal logic fundamentals
  • Time models and temporal logics
  • Temporal logic and real time
  • Formal specifications of embedded systems
  • Provers
  • Model checking
  • Real-time systems verification
  • Hybrid systems
  • Fieldbus-type protocols
  • Internet and embedded systems

Syllabus - others, projects and individual work of students

  • Essay based on selected scientific paper dealing with temporal logics as applied to topics of the students theses.

Controlled instruction

Written essay completing and defending.
Back to top