Title:

Specification of Embedded Systems

Code:SVD
Ac.Year:2012/2013
Sem:Winter
Curriculums:
ProgrammeFieldYearDuty
CSE-PHD-4DVI4-Elective
Language of Instruction:Czech
Completion:examination (verbal)
Type of
instruction:
Hour/semLecturesSeminar
Exercises
Laboratory
Exercises
Computer
Exercises
Other
Hours:390000
 ExamsTestsExercisesLaboratoriesOther
Points:00000
Guarantor:Š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.
Knowledge and skills required for the course:
  Basic lectures of mathematics at technical universities
Learning outcomes and competencies:
  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.
 

Your IPv4 address: 3.80.38.5
Switch to https

DNSSEC [dnssec]