|
On successful completion of the module, students should be able to:
-
Be aware of the need for formal methods and software verification.
-
Be familiar with a variety of well known model checkers. Have a working knowledge of relevant approaches to modelling and property specification.
-
Understand the fundamental principles underlying model checking.
-
Be able to use transition systems as a model for systems, and temporal logics to express system properties including functional correctness, reachability, safety, liveness, fairness and real-time properties.
-
Be able to specify and verify models using various approaches including PROMELA and SPIN, timed Automata and UPPAAL (realtime systems), and Petri nets.
|