Title:

Specification of Embedded Systems

Code:SVD
Ac.Year:2017/2018
Term:Winter
Curriculums:
ProgrammeBranchYearDuty
CSE-PHD-4DVI4-Elective
Language:Czech
Completion:examination (verbal)
Type of
instruction:
Hour/semLecturesSem. ExercisesLab. exercisesComp. exercisesOther
Hours:390000
 ExaminationTestsExercisesLaboratoriesOther
Points:00000
Guarantee:Švéda Miroslav, prof. Ing., CSc., DIFS
Lecturer:Švéda Miroslav, prof. Ing., CSc., DIFS
Faculty:Faculty of Information Technology BUT
Department:Department of Information Systems FIT BUT
 
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.
Description:
  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
Knowledge and skills required for the course:
  Basic lectures of mathematics at technical universities
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.
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.
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.
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.
Controlled instruction:
  Written essay completing and defending.