Title:  Specification of Embedded Systems 

Code:  SVD 

Ac.Year:  2017/2018 

Sem:  Winter 

Curriculums:  

Language of Instruction:  Czech 

Completion:  examination (verbal) 

Type of instruction:  Hour/sem  Lectures  Seminar Exercises  Laboratory Exercises  Computer Exercises  Other 

Hours:  39  0  0  0  0 

 Exams  Tests  Exercises  Laboratories  Other 

Points:  0  0  0  0  0 



Guarantor:  Š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 realtime systems; be aware of verification methods.  Description: 

  Embedded distributed system design principles stemming from behavioral formal specifications. Reactive systems and realtime systems: abstraction level, similarities and differencies. Reactive system and realtime system models: state sequences and trees, timedstate sequences; Kripke structures. Basic logical properties: fairness, livness, safety, feasibility; realtime 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. Realtime systems verification. Case studies.
Questions:
 Discrete systems theories: transformational, reactive and RT
 State sequence model of discrete systems behavior  properties: fairness, livness, safety
 Meanings and representation of the term "time"
 Timedstate sequence representation of the RT system behavior  properties: RT livness (nonZeno behavior), feasibility (machine closure), bounded response
 Time in distributed systems: a) Lamport model, logic clocks, physical clocks
 Modal and temporal logics, Kripke semantics
 Traditional proposition temporal logic, axiomatic base, its soundness and completness
 Proving and model checking
 Time models and propositional temporal logics
 RT extensions of temporal logic
 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 realtime systems; being informed about embedded distributed system architectures.  Syllabus of lectures: 


 Embedded distributed system design principles
 Reactive system and realtime system models
 Fairness, livness, safety, feasibility; realtime 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
 Realtime 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. SpringerVerlag, 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): RealTime: Theory in Practice. SpringerVerlag, LNCS 600, 1992.
 Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. SpringerVerlag, LNCS 827, 1994.
 Study literature: 


 Bowen J.P., Hinchey M.G.: HighIntegrity System Specification and Design. SpringerVerlag, 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. SpringerVerlag, 2004.
 de Bakker J.W. et all. (Editors): RealTime: Theory in Practice. SpringerVerlag, LNCS 600, 1992.
 Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. SpringerVerlag, LNCS 827, 1994.
 Johnsson B., Parrow J.: Formal Techniques in RealTime and Fault Tolerant Systems. SpringerVerlag, LNCS 1135, 1996.
 Controlled instruction: 

  Written essay completing and defending.  
