Course details
Formal Specifications of Computer-Based Systems
SSD Acad. year 2003/2004 Summer semester
Computer-based systems and their specifications. Selected topics of prerequisite course. Process algebras principles. Examples of process algebras. Real-time process algebras. Temporal logics review. Advanced principles of temporal specifications. 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 design.
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.