Title:

Formal Specifications of Computer-Based Systems

Code:SSD
Ac.Year:ukončen 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
 
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:
 
  • Computer-based systems and their specifications
  • Finite-state automata, omega-automata, timed automata
  • Process algebras principles, BPA; examples of process algebras, CSP, CCS 
  • Real-time 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; TLA as a real-time logic 
  • Proving
  • Model checking
  • Process algebras and temporal logics
  • Trace theory
  • Interrelations
  • Case studies
Syllabus - others, projects and individual work of students:
 
  • 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:
 
  • Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
  • Clarke E.M., Jr., Grumberg O., Peled D.A.: Model Checking. MIT Press, 2000.
  • Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
  • 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.
  • Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
  • Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2002.
Study literature:
 
  • Kreowski H.-J., Montanari U., Orejas F., Rozenberg G., Taentzer G.: Formal Methods in Software and Systems Modeling. Springer, LNCS 3393, 2005.
  • Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
  • Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
  • 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.
  • 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.
  • Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
  • 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.