Coursework

1. Write an essay which compares the conventional validation methods (e.g. simulation and testing) and formal verification, in particular model checking (app. 1000 words). The essay should at least contain the following aspects:

(a) what is model checking and how it works

(b) its difference between simulation and testing

(c) what particular systems model checking is used for

(d) its use in industry, state of art tools, etc.

You are required to provide references to the sources used to produce your work. For the referencing style please refer to the module descriptor.

2. Assume that a retail company has two storage units: a primary and a secondary unit. The warehouse controller monitors the goods that comes in, directs them to the primary storage unit first and moves the goods from the primary unit to the secondary when necessary. The process works as follows:

- Initially both storage units are empty.
- New goods may be brought into the primary storage unit at any point in time (new goods are not stored in the secondary unit in the first place).
- When some goods exist in the primary unit, the controller starts moving them from the primary unit to the secondary unit.
- If a storage unit is empty, it cannot be made full in the next step. Similarly, if a storage unit is full, it cannot be emptied in the next step.
- If the primary unit becomes empty or the secondary unit becomes full, it is not possible to transfer any goods from the primary unit to the secondary unit.

(a) Draw the state machine that describes the system.

Hint: Assume that there are two state variables, one for each storage unit, which can take any of the following values: empty, partially full, or full.
(b) Express the following property in LTL and CTL:
It is not possible that the secondary storage unit stays partially full forever.
(c) Using the CTL model checking algorithm prove that the CTL formula in b) is verified or not.
(d) Write a property of your own, express it in CTL and LTL, where possible, and show if it can be verified.

Remark: You do not have to use the labelling algorithm or automata theoretic model checking algorithm. A proof using execution paths (as described in "Lecture 5: LTL and CTL") is acceptable.