Title:

Formal Specifications of Computer-Based Systems

Code:SSD
Ac.Year:2008/2009
Term:Summer
Curriculums:
ProgrammeBranchYearDuty
CSE-PHD-4DVI4-Elective
IT-PHD-3DIT3-Elective
Language:Czech
Completion:examination (verbal)
Type of
instruction:
Hour/semLecturesSem. ExercisesLab. exercisesComp. exercisesOther
Hours:390000
 ExaminationTestsExercisesLaboratoriesOther
Points:00000
Guarantee:Švéda Miroslav, prof. Ing., CSc., DIFS
Faculty:Faculty of Information Technology BUT
Department:Department of Information Systems FIT BUT
Prerequisites: 
Embedded System Specification (SVS), DIFS
 
Learning objectives:
Be aware of current formal specification principles as applied to computer-based systems and their componets design.
Description:
The aim of this course is to offer a review of typical formal tools utilizable for behavioral specifications of Computer-based systems and their components. After passing the review, every student should select a proper tool applicable for his dissertation thema and study it in more detail. The review covers subdomains with the following examples of tool and method: Finite-state automata, omega-automata, timed automata. Process algebra principles with BPA. Examples of process algebras: CSP, CCS. Timed process algebras, TCSP. Temporal logics review. Temporal specifications of the following types of properties: reachability, safety, liveness, fairness, bounded response time, .... Examples of real-time temporal logics. Proving and model checking interplay. Process algebras and temporal logics. Trace theory and other theories. Interrelations. Case studies.
Knowledge and skills required for the course:
Basic lectures of mathematics at technical universities
Learning outcomes and competences:
Being informed about current formal specification principles as applied to computer-based systems design.
Syllabus of lectures:
  1. Computer-based systems and their specifications
  2. Finite-state automata, omega-automata, timed automata
  3. Process algebras principles, BPA; examples of process algebras, CSP, CCS 
  4. Real-time process algebras, TCSP 
  5. Temporal logics review
  6. Temporal specifications of the following types of properties: reachability, safety, liveness, fairness, bounded response time, ...
  7. Examples of real-time temporal logics; TLA as a real-time logic 
  8. Proving
  9. Model checking
  10. Process algebras and temporal logics
  11. Trace theory
  12. Interrelations
  13. Case studies
Syllabus - others, projects and individual work of students:
  1. Essay based on selected formal tool dealing with automata, process algebras, or temporal logics as applied to topics of the student's theses.
Fundamental literature:
  1. Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
  2. Clarke E.M., Jr., Grumberg O., Peled D.A.: Model Checking. MIT Press, 2000.
  3. Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
  4. de Bakker J.W., de Roever W.-P., Rozenberg G. (Editors): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer-Verlag, LNCS 354, 1989.
  5. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
  6. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2002.
Study literature:
  1. Kreowski H.-J., Montanari U., Orejas F., Rozenberg G., Taentzer G.: Formal Methods in Software and Systems Modeling. Springer, LNCS 3393, 2005.
  2. Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
  3. Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  4. Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
  5. Abramsky S., Gabbay D.M., Maibaum T.S.E. (Editors): Handbook of Logic in Computer Science. Volumes 1, 2, 3, 4, 5. Oxford Science Publications, 2000.
  6. de Bakker J.W., de Roever W.-P., Rozenberg G. (Editors): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer-Verlag, LNCS 354, 1989.
  7. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
  8. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2002.
Controlled instruction:
Written essay completing and defending.