Course details
Specification of Embedded Systems
SVD Acad. year 2007/2008 Winter semester
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.
Guarantor
Language of instruction
Completion
Time span
- 39 hrs lectures
Department
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 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
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.