Course details

Formal Specifications of Computer-Based Systems

SSD Acad. year 2006/2007 Summer semester

Current academic year

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.

Guarantor

Švéda Miroslav, prof. Ing., CSc.

Language of instruction

Czech

Completion

Examination

Time span

  • 39 hrs lectures

Department

Department of Information Systems (UIFS)

Subject specific learning outcomes and competences

Being informed about current formal specification principles as applied to computer-based systems design.

Learning objectives

Be aware of current formal specification principles as applied to computer-based systems and their componets design.

Prerequisite knowledge and skills

Basic lectures of mathematics at technical universities

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.

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.

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

Progress assessment

Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.

Controlled instruction

Written essay completing and defending.

Back to top