Question 1 (10 marks): Explain why security protocols are a good example of a domain where model checking techniques may be applied successfully.

Question 2 (10 marks): What is busy-waiting in multi-threading programming? Discuss when it can be useful in improving the performance of a multi-threading application, and when it can reduce the performance.

Question 3 (10 marks): Discuss the roles and differences of traditional testing, model checking and theorem proving, and why they cannot replace each other.