Course details

Specification of Embedded Systems

SVD Acad. year 2017/2018 Winter semester

Current academic year

Embedded distributed system design principles stemming from behavioral formal specifications. Reactive systems and real-time systems: abstraction level, similarities and differencies. Reactive system and real-time system models: state sequences and trees, timed-state sequences; Kripke structures. Basic logical properties: fairness, livness, safety, feasibility; real-time livness, bounded time response. Modal logics and temporal logics: Kripke semantics. Temporal logic fundamentals: syntax, semantics, axiomatics. Time models and temporal logics: order, future x past, discrete x dense x continuous, time origin, time end. LTL. CTL. Temporal logic and real time: observation sequences; approach by Alur and Henzinger; approach by Koymans and Vytopil and de Roever; approach by Pnueli and de Roever. Formal specifications of embedded systems. Provers. Model checking. Real-time systems verification. Case studies.

Questions:

  1. Discrete systems theories: transformational, reactive and RT
  2. State sequence model of discrete systems behavior - properties: fairness, livness, safety
  3. Meanings and representation of the term "time"
  4. Timed-state sequence representation of the RT system behavior - properties: RT livness (non-Zeno behavior), feasibility (machine closure), bounded response
  5. Time in distributed systems: a) Lamport model, logic clocks, physical clocks
  6. Modal and temporal logics, Kripke semantics
  7. Traditional proposition temporal logic, axiomatic base, its soundness and completness
  8. Proving and model checking
  9. Time models and propositional temporal logics
  10. RT extensions of temporal logic

Guarantor

Švéda Miroslav, prof. Ing., CSc.

Language of instruction

Czech

Completion

Examination (oral)

Department

Department of Information Systems (UIFS)

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 verification methods.

Prerequisite knowledge and skills

Basic lectures of mathematics at technical universities

Study literature

  • Bowen J.P., Hinchey M.G.: High-Integrity System Specification and Design. Springer-Verlag, 1999.
  • Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2000.
  • Schneider K.: Verification of Reactive Systems -- Formal Methods and Algorithms. Springer-Verlag, 2004.
  • 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.
  • Johnsson B., Parrow J.: Formal Techniques in Real-Time and Fault Tolerant Systems. Springer-Verlag, LNCS 1135, 1996.

Fundamental literature

  • Schneider K.: Verification of Reactive Systems -- Formal Methods and Algorithms. Springer-Verlag, 2004.
  • Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2000.
  • 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 seminars

Syllabus of lectures:
  • Embedded distributed system design principles
  • Reactive system and real-time system models
  • Fairness, livness, safety, feasibility; real-time livness, bounded time response
  • Temporal logic fundamentals: syntax, semantics, axiomatics
  • Time models and temporal logics
  • LTL
  • CTL
  • Temporal logic and real time
  • Formal specifications of embedded systems
  • Provers
  • Model checking
  • Real-time systems verification
  • Case studies

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.

Progress assessment

Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.

Controlled instruction

Written essay completing and defending.

Course inclusion in study plans

  • Programme VTI-DR-4, field DVI4, any year of study, Elective
Back to top