Course detail
Formal Specifications of Computer-Based Systems
FIT-SSDAcad. year: 2015/2016
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:
- Discrete state system and its behavior
- Theorem verifications in predicate logic
- Finite automata-based 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
- Model-checker example
- Formal specs problems in real-world applications and approaches how to solve them
Language of instruction
Mode of study
Guarantor
Department
Learning outcomes of the course unit
Prerequisites
Co-requisites
Planned learning activities and teaching methods
Assesment methods and criteria linked to learning outcomes
Course curriculum
- 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
- Essay based on selected formal tool dealing with automata, process algebras, or temporal logics as applied to topics of the student's theses.
Syllabus - others, projects and individual work of students:
Work placements
Aims
Specification of controlled education, way of implementation and compensation for absences
Recommended optional programme components
Prerequisites and corequisites
Basic literature
Recommended reading
Classification of course in study plans
Type of course unit
Lecture
Teacher / Lecturer
Syllabus
- 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