Title:  Formal Specifications of ComputerBased Systems 

Code:  SSD 

Ac.Year:  ukončen 2015/2016 

Sem:  Summer 

Curriculums:  

Language of Instruction:  Czech 

Completion:  examination (oral) 

Type of instruction:  Hour/sem  Lectures  Seminar Exercises  Laboratory Exercises  Computer Exercises  Other 

Hours:  39  0  0  0  0 

 Exams  Tests  Exercises  Laboratories  Other 

Points:  0  0  0  0  0 



Guarantor:  Švéda Miroslav, prof. Ing., CSc. (DIFS) 

Lecturer:  Š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 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.
Questions:
 Discrete state system and its behavior
 Theorem verifications in predicate logic
 Finite automatabased formal models
 LTL and CTL temporal logics  principles
 CSP process algebra  principles
 Formal models with time  examples
 Property specifications of the types: reachability, safety, liveness, bounded response time
 Example properties verification in formal models
 Modelchecker example
 Formal specs problems in realworld applications and approaches how to solve them
 Knowledge and skills required for the course: 

  Basic lectures of mathematics at technical universities  Learning outcomes and competencies: 

  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.  
