Defects in safety-critical software systems can cause large economical and other losses.
Often these systems are far too complex to be tested extensively. In this work a formal
verification technique called model checking is utilized. In the technique, a mathematical
model is created that captures the essential behaviour of the system. The specifications of
the system are stated in some formal language, usually temporal logic. The behaviour of the
model can then be checked exhaustively against a given specification. This report studies …