Title:  Formal Specifications of ComputerBased Systems 

Code:  SSD 

Ac.Year:  2008/2009 

Term:  Summer 

Curriculums:  

Language:  Czech 

Completion:  examination (verbal) 

Type of instruction:  Hour/sem  Lectures  Sem. Exercises  Lab. exercises  Comp. exercises  Other 

Hours:  39  0  0  0  0 

 Examination  Tests  Exercises  Laboratories  Other 

Points:  0  0  0  0  0 



Guarantee:  Švéda Miroslav, prof. Ing., CSc., DIFS 

Faculty:  Faculty of Information Technology BUT 

Department:  Department of Information Systems FIT BUT 

Prerequisites:  

 Learning objectives: 

  Be aware of current formal specification principles as applied to computerbased 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 Computerbased 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: Finitestate automata, omegaautomata, 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 realtime 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 computerbased systems design.  Syllabus of lectures: 



 Computerbased systems and their specifications
 Finitestate automata, omegaautomata, timed automata
 Process algebras principles, BPA; examples of process algebras, CSP, CCS
 Realtime process algebras, TCSP
 Temporal logics review
 Temporal specifications of the following types of properties: reachability, safety, liveness, fairness, bounded response time, ...
 Examples of realtime temporal logics; TLA as a realtime 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. SpringerVerlag, 2001.
 Clarke E.M., Jr., Grumberg O., Peled D.A.: Model Checking. MIT Press, 2000.
 Schneider K.: Verification of Reactive Systems. SpringerVerlag, 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. SpringerVerlag, LNCS 354, 1989.
 Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. SpringerVerlag, 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. SpringerVerlag, 2001.
 Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
 Schneider K.: Verification of Reactive Systems. SpringerVerlag, 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. SpringerVerlag, LNCS 354, 1989.
 Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. SpringerVerlag, 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.  
