Experiences with Specification and Verification in LOTOS:
A Report on Two Case Studies
We consider the problems of verifying properties of LOTOS specifications
with specific reference to two case studies, one of which was proposed
by an industrial collaborator. The case studies present quite different
verification requirements and we study a range of verification and
validation techniques, based on various behavioural congruences and
preorders, which may be applied, also using some mechanised tool support.
We consider the implications of the (formal) proofs which succeed or fail
with respect to our desired properties, and draw some conclusions about
the verification process.
Dr Carron Shankland
Last revision: 27th January 1997