Title:

Embedded System Specification

Code:SVSe
Ac.Year:2009/2010
Term:Summer
Study plans:
ProgramBranchYearDuty
IT-MSC-2MBI-Elective
IT-MSC-2MBS-Compulsory-Elective - group C
IT-MSC-2MGM-Elective
IT-MSC-2MGM.-Elective
IT-MSC-2MIN-Elective
IT-MSC-2MIN.-Elective
IT-MSC-2MIS-Compulsory-Elective - group F
IT-MSC-2MIS.1stElective
IT-MSC-2MMI1stCompulsory-Elective - group M
IT-MSC-2MMM-Elective
IT-MSC-2MPS-Elective
IT-MSC-2MPV-Elective
IT-MSC-2MSK2ndCompulsory-Elective - group C
IT-MSC-2EITE2ndElective
Language:English
Credits:5
Completion:examination (written)
Type of
instruction:
Hour/semLecturesSem. ExercisesLab. exercisesComp. exercisesOther
Hours:390067
 ExaminationTestsExercisesLaboratoriesOther
Points:60150025
Guarantee:Švéda Miroslav, prof. Ing., CSc., DIFS
Lecturer:Ryšavý Ondřej, Ing., Ph.D., DIFS
Švéda Miroslav, prof. Ing., CSc., DIFS
Instructor:Ryšavý Ondřej, Ing., Ph.D., DIFS
Faculty:Faculty of Information Technology BUT
Department:Department of Information Systems FIT BUT
Substitute for:
Computer Communications and Interfacing (KPA), DIFS
 
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 embedded distributed system architectures.
Description:
Embedded distributed system design principles. Reactive systems and real-time systems. Reactive system and real-time system models. Fairness, livness, safety, feasibility; real-time livness. Temporal logic fundamentals. Time models and temporal logics. Temporal logic and real time. Formal specifications of embedded systems. Hybrid systems. Provers. Model checking. Real-time systems verification.
Knowledge and skills required for the course:
Propositional logic. Basics of the first-order 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 real-time systems; being informed about embedded distributed system architectures.
Generic learning outcomes and competences:
Being acknowledged with basics of temporal logic.
Syllabus of lectures:
  1. Embedded distributed system design principles
  2. Reactive system and real-time system models
  3. Fairness, livness, safety, feasibility; real-time livness
  4. Temporal logic fundamentals
  5. Time models and temporal logics
  6. Temporal logic and real time
  7. Formal specifications of embedded systems
  8. Provers
  9. Model checking
  10. Real-time systems verification
  11. Formal specification of abstract data types and objects, algebraic specifications
  12. Using type theoretic systems for formal specification and verification of programs
Syllabus of numerical exercises:
 
Syllabus of laboratory exercises:
 
Syllabus of computer exercises:
  1. Introduction to TLA+, and method B
  2. TLA+ case studies
  3. Method B case studies
Syllabus - others, projects and individual work of students:
  1. Specification and verification of embedded system properties using TLA+ or Method B
Fundamental literature:
  1. Schneider, K.: Verification of Reactive Systems, Springer-Verlag, 2004, ISBN 3-540-00296-0
  2. Huth, M.R.A., Ryan, M.D.: Logic in Computer Science - Modelling and Reasoning about Systems, Cambridge University Press, 2002, ISBN 0-521-65602-8
  3. Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8
  4. de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1
  5. Gabbay, D.M., Ohlbach, H.J. (Editors): Temporal Logic, Springer-Verlag, LNCS 827, 1994, ISBN 3-540-58241-X
  6. Monin, J.F., Hinchey, M.G.:Understanding Formal Methods, Springer-Verlang, 2003.
  7. Peled, D.A.:Software Reliability Methods, Text in Computer Science, Springer, 2001.
  8. Tennent, R.D.:Specifying Software: A Hand-On Introduction, Cambridge University Press, 2002.
  9. Bertot, Y., Casteran, P.:Interactive Theorem Proving and Program Development, Springer-Verlang, 2004.
Study literature:
  1. Huth, M.R.A., Ryan, M.D.: Logic in Computer Science - Modelling and Reasoning about Systems, Cambridge University Press, 2002, ISBN 0-521-65602-8
  2. Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8
  3. de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1
Links:
SVSe/private/index.html
Controlled instruction:
Mid-term exam, laboratory practice supported by project work, and final exam are the monitored, and points earning, education. Mid-term exam and laboratory practice are without correction eventuality. Final exam has two additional correction eventualities. 
Progress assessment:
Written mid-term exam and submitting project in a due date.
Exam prerequisites:
Requirements for class accreditation are not defined.