Title:

Formal Specifications of Computer-Based Systems

Code:SSD
Ac.Year:ukončen 2015/2016
Sem:Summer
Curriculums:
ProgrammeField/
Specialization
YearDuty
CSE-PHD-4DVI4-Elective
Language of Instruction:Czech
Completion:examination (oral)
Type of
instruction:
Hour/semLecturesSeminar
Exercises
Laboratory
Exercises
Computer
Exercises
Other
Hours:390000
 ExamsTestsExercisesLaboratoriesOther
Points:00000
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 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.

Questions:

  1. Discrete state system and its behavior
  2. Theorem verifications in predicate logic
  3. Finite automata-based formal models
  4. LTL and CTL temporal logics - principles
  5. CSP process algebra - principles
  6. Formal models with time - examples
  7. Property specifications of the types: reachability, safety, liveness, bounded response time
  8. Example properties verification in formal models
  9. Model-checker example
  10. Formal specs problems in real-world 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 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.
 

Your IPv4 address: 54.81.220.239
Switch to https