Course details
Formal Specifications of Computer-Based Systems
SSD Acad. year 2012/2013 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
Completion
Time span
- 39 hrs lectures
Department
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.