Course detail

Embedded System Specification

FIT-SVSeAcad. year: 2015/2016

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.

Language of instruction

English

Number of ECTS credits

5

Mode of study

Not applicable.

Guarantor

prof. Ing. Miroslav Švéda, CSc.

Department

Department of Information Systems (UIFS)

Learning outcomes of the course unit

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.

Being acknowledged with basics of temporal logic.

Prerequisites

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

Co-requisites

Not applicable.

Planned learning activities and teaching methods

Not applicable.

Assesment methods and criteria linked to learning outcomes

Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.

Requirements for class accreditation are not defined.

Course curriculum

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 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

Work placements

Not applicable.

Aims

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.

Specification of controlled education, way of implementation and compensation for absences

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. 

Recommended optional programme components

Not applicable.

Prerequisites and corequisites

Not applicable.

Basic 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.

Recommended reading

  • 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

Classification of course in study plans

  • Programme IT-MGR-2 Master's

    branch MBI , any year of study, summer semester, elective
    branch MPV , any year of study, summer semester, elective
    branch MGM , any year of study, summer semester, elective
    branch MIS , any year of study, summer semester, compulsory-optional
    branch MBS , any year of study, summer semester, compulsory-optional
    branch MIN , any year of study, summer semester, elective
    branch MMI , any year of study, summer semester, compulsory-optional
    branch MMM , any year of study, summer semester, elective

  • Programme IT-MGR-1H Master's

    branch MGH , any year of study, summer semester, recommended

  • Programme IT-MGR-2 Master's

    branch MSK , 2. year of study, summer semester, compulsory-optional

Type of course unit

 

Lecture

26 hours, optionally

Teacher / Lecturer

prof. Ing. Miroslav Švéda, CSc.

Syllabus

  • 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

Exercise in computer lab

8 hours, optionally

Teacher / Lecturer

prof. Ing. Miroslav Švéda, CSc.

Syllabus

  • Spin, model checking techniques
  • PVS, theorem proving techniques

Project

10 hours, optionally

Teacher / Lecturer

prof. Ing. Miroslav Švéda, CSc.