Title:  Embedded System Specification 

Code:  SVSe 

Ac.Year:  2012/2013 

Term:  Summer 

Curriculums:  

Language:  English 

Credits:  5 

Completion:  examination (written&verbal) 

Type of instruction:  Hour/sem  Lectures  Sem. Exercises  Lab. exercises  Comp. exercises  Other 

Hours:  39  0  0  6  7 

 Examination  Tests  Exercises  Laboratories  Other 

Points:  60  15  0  0  25 



Guarantee:  Švéda Miroslav, prof. Ing., CSc., DIFS 

Lecturer:  Ryšavý Ondřej, doc. Ing., Ph.D., DIFS Švéda Miroslav, prof. Ing., CSc., DIFS 
Instructor:  Ryšavý Ondřej, doc. Ing., Ph.D., DIFS 

Faculty:  Faculty of Information Technology BUT 

Department:  Department of Information Systems FIT BUT 

Substitute for:  

 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 embedded distributed system architectures.  Description: 

Embedded distributed system design principles. Reactive systems and realtime systems. Reactive system and realtime system models. Fairness, livness, safety, feasibility; realtime livness. Temporal logic fundamentals. Time models and temporal logics. Temporal logic and real time. Formal specifications of embedded systems. Hybrid systems. Provers. Model checking. Realtime systems verification.  Knowledge and skills required for the course: 

Propositional logic. Basics of the firstorder logic. The elementary notions of communication protocols.  Subject specific learning outcomes and competences: 

Understanding behavioral formal specifications as applied to embedded systems design; being aware of utilizing temporal logics for modeling reactive systems and realtime systems; being informed about embedded distributed system architectures.  Generic learning outcomes and competences: 

Being acknowledged with basics of temporal logic.  Syllabus of lectures: 

 Embedded distributed system design principles
 Reactive system and realtime system models
 Fairness, livness, safety, feasibility; realtime livness
 Temporal logic fundamentals
 Time models and temporal logics
 Temporal logic and real time
 Formal specifications of embedded systems
 Provers
 Model checking
 Realtime systems verification
 Formal specification of abstract data types and objects, algebraic specifications
 Using type theoretic systems for formal specification and verification of programs
 Syllabus of numerical exercises: 

 Introductory to system Coq. Brief exploration of formalism of the system, description of mathematical vernacular  the language used for communicating with the system, demonstration of the system for specifying and verifying properties of a simple algorithm.
 Syllabus of laboratory exercises: 

 Embedded application management with intranet
 Syllabus of computer exercises: 

 Spin, model checking techniques
 PVS, theorem proving techniques
 Syllabus  others, projects and individual work of students: 

 Specification and verification of embedded system properties
 Fundamental literature: 

 Schneider, K.: Verification of Reactive Systems, SpringerVerlag, 2004, ISBN 3540002960
 Huth, M.R.A., Ryan, M.D.: Logic in Computer Science  Modelling and Reasoning about Systems, Cambridge University Press, 2002, ISBN 0521656028
 Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0262032708
 de Bakker, J.W. et all. (Editors): RealTime: Theory in Practice, SpringerVerlag, LNCS 600, 1992, ISBN 3540555641
 Gabbay, D.M., Ohlbach, H.J. (Editors): Temporal Logic, SpringerVerlag, LNCS 827, 1994, ISBN 354058241X
 Monin, J.F., Hinchey, M.G.:Understanding Formal Methods, SpringerVerlang, 2003.
 Peled, D.A.:Software Reliability Methods, Text in Computer Science, Springer, 2001.
 Tennent, R.D.:Specifying Software: A HandOn Introduction, Cambridge University Press, 2002.
 Bertot, Y., Casteran, P.:Interactive Theorem Proving and Program Development, SpringerVerlang, 2004.
 Study literature: 

 Huth, M.R.A., Ryan, M.D.: Logic in Computer Science  Modelling and Reasoning about Systems, Cambridge University Press, 2002, ISBN 0521656028
 Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0262032708
 de Bakker, J.W. et all. (Editors): RealTime: Theory in Practice, SpringerVerlag, LNCS 600, 1992, ISBN 3540555641
 Controlled instruction: 

Midterm exam, laboratory practice supported by project work, and final exam are the monitored, and points earning, education. Midterm exam and laboratory practice are without correction eventuality. Final exam has two additional correction eventualities.  Progress assessment: 

Protocol about a lab experiment, written midterm exam and submitting project in a due date.  Exam prerequisites: 

Requirements for class accreditation are not defined.  
