This paper shows how reactive systems can be modelled and analysed using finite-state machines and temporal logic, and how model checking tools can be used to verify crucial properties of safety-critical systems. The paper also provides an introduction into the algorithms and data structures used to model check very large finite-state systems.
There will be assignments to practice the use of two different model checkers, and a test will assess the theoretical aspects of temporal logic and model checking algorithms. During a final assignment, students will have the opportunity to build their own model checker.
COMP235 Logic and Computation and
60 points at 300 level in Computer Science
Students entering this paper are expected to know about propositional logic and finite-state machines. The final assignment requires Java programming skils.
COMP552 Model Checking
Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Systems and Software Verification, Springer, 2001.
Michael Huth, Mark Ryan, Logic in Computer Science, 2nd edition, Cambridge University Press, 2004.
Internal assessment/final examination ratio 1:0