Faculty of Information Technology, BUT

Course details

Formal Specifications of Computer-Based Systems

SSD Acad. year 2007/2008 Summer semester

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

Language of instruction

Czech

Completion

Examination (oral)

Time span

39 hrs lectures

Assessment points

Department

Lecturer

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 kwnowledge 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

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.

Controlled instruction

Written essay completing and defending.

Course inclusion in study plans

Back to top