Embedded System Specification

• 39 hrs lectures
• 6 hrs pc labs
• 7 hrs projects

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.

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.

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

• 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
• Peregrin, J.: Logika a logiky, Academia, 2004, ISBN 80-200-1187-0

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

• 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

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

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.

Teaching methods depend on the type of course unit as specified in the article 7 of BUT Rules for Studies and Examinations.

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.