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

Author

Kirkwood, Carron ; Thomas, Muffy

Author_Institution

Dept. of Comput. Sci., Glasgow Univ., UK

fYear

1995

fDate

5-8 Apr 1995

Firstpage

159

Lastpage

171

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

Keywords

formal specification; program verification; software tools; specification languages; LOTOS; LOTOS specifications; behavioural congruences; formal proof; specification; tool support; validation techniques; verification; verification process; verification requirements; Carbon capture and storage; Collaboration; Communication system control; Computer aided software engineering; Protocols; Radio control; System recovery; System testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Industrial-Strength Formal Specification Techniques, 1995. Proceedings., Workshop on

Conference_Location

Boca Raton, FL

Print_ISBN

0-8186-7005-3

Type

conf

DOI

10.1109/WIFT.1995.515487

Filename

515487