Conference Proceeding

Experiences with specification and verification in LOTOS: a report on two case studies

Citation

Shankland C & Thomas M (1995) Experiences with specification and verification in LOTOS: a report on two case studies. In: Workshop on Industrial-Strength Formal Specification Techniques, 1995. Proceedings. Workshop on Industrial-Strength Formal Specification Techniques, 1995, Boca Raton, FL, USA, 05.04.1995-08.04.1995. Los Alamitos, CA, USA: IEEE Computer Society Press, pp. 159-171. http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=515487&tag=1; https://doi.org/10.1109/WIFT.1995.515487

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 which may be applied, based on various behavioural congruences and preorders, 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.

StatusPublished
Publication date31/12/1995
Publication date online30/04/1995
PublisherIEEE Computer Society Press
Publisher URLhttp://ieeexplore.ieee.org/…ber=515487&tag=1
Place of publicationLos Alamitos, CA, USA
ISBN0-8186-7005-3
ConferenceWorkshop on Industrial-Strength Formal Specification Techniques, 1995
Conference locationBoca Raton, FL, USA
Dates