Specifying and proving safety properties in FOREST

The FOREST project involved the development of a technique for the formal specification of requirements, intended for use in real time embedded systems, especially where safety is an important issue. It was considered that the project must develop a suitable formal notation for expressing requirements, together with a targetted method for eliciting requirements and expressing them in the notation. To validate specifications, two tools have been developed, an automatic theorem prover and an animator. The latter can be viewed as testing that the specified behaviour does correspond to the intended one, given some starting conditions, and, while giving a graphic demonstration of the effects specified, has the limitation of all testing that it tests only a subset of possible situations. It was decided that to provide a complete system specification, the notation must concern itself with identifying the components of the system, and their actions and must be able to describe not only the functionality of each action, what it does for the system, but also what causes it to happen, what circumstances enable or trigger its occurrence, roughly why it happens, and finally determine temporal constraints determining when it may, must or must not occur. The selected notation is a logic called modal action logic (MAL). The author discusses MAL and the theorem prover