Faculty of Information Technology, BUT

Course details

Embedded System Specification

SVSe Acad. year 2015/2016 Summer semester 5 credits

Course is not open in this year
Close
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.

Guarantor

Language of instruction

English

Completion

Examination (written+oral)

Time span

26 hrs lectures, 8 hrs pc labs, 10 hrs projects

Assessment points

60 exam, 15 half-term test, 25 projects

Department

Lecturer

Instructor

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.

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.

Prerequisite kwnowledge and skills

Propositional logic. Basics of the first-order logic. The elementary notions of communication protocols.

Study literature

  • 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
  • Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8
  • de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1

Fundamental literature

  • Schneider, K.: Verification of Reactive Systems, Springer-Verlag, 2004, ISBN 3-540-00296-0
  • 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
  • Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8
  • de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1
  • Gabbay, D.M., Ohlbach, H.J. (Editors): Temporal Logic, Springer-Verlag, LNCS 827, 1994, ISBN 3-540-58241-X
  • Monin, J.F., Hinchey, M.G.:Understanding Formal Methods, Springer-Verlang, 2003.
  • Peled, D.A.:Software Reliability Methods, Text in Computer Science, Springer, 2001.
  • Tennent, R.D.:Specifying Software: A Hand-On Introduction, Cambridge University Press, 2002.
  • Bertot, Y., Casteran, P.:Interactive Theorem Proving and Program Development, Springer-Verlang, 2004.

Syllabus of lectures

  • Embedded distributed system design principles
  • 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
  • Provers
  • Model checking
  • Real-time 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 - others, projects and individual work of students

  • Specification and verification of embedded system properties

Progress assessment

Protocol about a lab experiment, written mid-term exam and submitting project in a due date.

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. 

Exam prerequisites

Requirements for class accreditation are not defined.

Course inclusion in study plans

  • Programme IT-MSC-2, field MBI, MGM, MIN, MMM, MPV, any year of study, Elective
  • Programme IT-MSC-2, field MBS, any year of study, Compulsory-Elective group C
  • Programme IT-MSC-2, field MIS, any year of study, Compulsory-Elective group F
  • Programme IT-MSC-2, field MMI, any year of study, Compulsory-Elective group M
  • Programme IT-MSC-2, field MSK, 2nd year of study, Compulsory-Elective group C
Back to top