Experiences with Specification and Verification in LOTOS:
A Report on Two Case Studies

Abstract

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.

[] Research   [] Teaching   [] CV   [] Personal   [Home] Home
Dr Carron Shankland    Email: ces@cs.stir.ac.uk [email me]    Last revision: 27th January 1997