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

• 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

• Introduction to TLA+, and method B
• TLA+ case studies
• Method B case studies

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.

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.