Title:

Embedded System Specification

Code:SVSe
Ac.Year:2012/2013
Term:Summer
Curriculums:
ProgrammeBranchYearDuty
IT-MSC-2MBI-Elective
IT-MSC-2MBS-Compulsory-Elective - group C
IT-MSC-2MGM-Elective
IT-MSC-2MIN-Elective
IT-MSC-2MIS-Compulsory-Elective - group F
IT-MSC-2MMI-Compulsory-Elective - group M
IT-MSC-2MMM-Elective
IT-MSC-2MPV-Elective
IT-MSC-2MSK2ndCompulsory-Elective - group C
IT-MSC-2EITE2ndElective
Language:English
Credits:5
Completion:examination (written&verbal)
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, doc. Ing., Ph.D., DIFS
Švéda Miroslav, prof. Ing., CSc., DIFS
Instructor:Ryšavý Ondřej, doc. 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:
 
  • 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
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.
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
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:
  Protocol about a lab experiment, written mid-term exam and submitting project in a due date.
Exam prerequisites:
  Requirements for class accreditation are not defined.