|
Lecturer(s)
|
-
Jančar Petr, prof. RNDr. CSc.
|
|
Course content
|
1. Introduction. Reactive systems, examples. Transition systems as the basic model. Calculus of communicating systems (CCS) informally. 2. Syntax and semantics of CCS, examples. CCS with variables. 3. Behavioural equivalences. Trace equivalence. Bisimulation equivalence. 4. Properties of strong bisimilarity. Internal actions. Weak bisimilarity. Example on a small communication protocol. 5. Software tool Concurrency Workbench, CWB (Edinburgh, UK). Modal logic HML (Henessy-Milner Logic); description of simple behavioural properties. 6. Further examples in CWB. Correspondence of bisimulation equivalence and HM-logic. Fixed points in complete lattices for semantics of recursive programs. 7. Bisimulation equivalence as a fixed point. HM-logic with recursion and its game characterization. 8. A small project: alternating bit protocol in CCS and its verification in CWB. 9. Timed transition systems. Timed CCS and timed automata. 10. Timed and untimed bisimulation equivalence. Regions at timed automata. HM-logic with time. 11. Software tool UPPAAL (based on timed automata). Modelling, specification, simulation and verification in UPPAALu on practical examples. 12. Small project: `gossiping girls' in UPPAAL. 13. Overview of other areas of verification.
|
|
Learning activities and teaching methods
|
|
Lecture, Laboratory Work
|
|
Learning outcomes
|
Students get concrete experience with program verification and knowledge of the respective theoretical background.
1. Knowledge Describe and comprehensively understand principles of verification of concurrent programs.
|
|
Prerequisites
|
unspecified
|
|
Assessment methods and criteria
|
Oral exam, Seminar Work
Active participation in class. Completion of assigned homeworks, in particular two small projects. Passing the oral (or written) exam.
|
|
Recommended literature
|
-
Volně dostupné tutoriály k verifikačním nástrojům (CWB, UPPAAL).
-
Aceto L., Ingólfsdóttir A., Larsen K.G., Srba J. (2007). Reactive Systems: Modelling, Specification and Verification. Cambridge University Press.
-
Baier C., Katoen J.-P. (2008). Principles of Model Checking. The MIT Press.
-
Clarke E.M., Henzinger T.A., Veith H., and Bloem R. (2018). Handbook of Model Checking. Springer.
-
Clarke M., Grumberg O. and Peled D. A. (2000). Model checking. The MIT Press.
-
Manna Z. (1981). Matematická teorie programů. SNTL Praha.
-
Peled D. (2001). Software Reliability Methods. Springer.
-
Schneider K. (2004). Verification of Reactive Systems: Formal Methods and Algorithms. Springer.
|