Formal Specifications of Computer-Based Systems

Guarantor

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

Language of instruction

Czech

Completion

Examination

Time span

Department

Department of Information Systems (UIFS)

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

Course inclusion in study plans