A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol

Tim Willemse; Jan Tretmans; Arjen Klomp

A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol

Tim Willemse, Jan Tretmans, Arjen Klomp

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

This paper reports on the results of the application of formal methods in the development of an industrial, mission-critical system, called the Operator Support System. A critical communication protocol of this system, the OM/RR Protocol, and its corresponding service were formalised using the formal specification language Lotos. The resulting specifications have been validated using the tool set Lite and models of the specifications, obtained by making abstractions, have been verified using the tool Eucalyptus. Whereas the use of formal methods is usually motivated by their ability to allow for unambiguous and precise system descriptions amenable to mathematical reasoning, it turned out that in this project most benefits were obtained by the sheer process of formalising the informal protocol description, revealing many omissions and ambiguities. The results and experiences obtained during formalisation, validation, abstraction and verification are discussed on a non-formal basis in this paper.

Original language	English
Title of host publication	5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
Editors	Stefania Gnesi, Ina Schieferdecker, Axel Rennoch
Publisher	G.M.D.
Pages	331-344
Number of pages	14
Publication status	Published - 2000
Event	5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000 - Berlin, Germany Duration: 3 Apr 2000 → 4 Apr 2000 Conference number: 5 https://fmics.inria.fr/workshop-5/

Publication series

Name	GMD Report
Publisher	GMD
Volume	91
ISSN (Print)	1435-2702

Workshop

Workshop	5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
Abbreviated title	FMICS
Country/Territory	Germany
City	Berlin
Period	3/04/00 → 4/04/00
Internet address	https://fmics.inria.fr/workshop-5/

Keywords

FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

Cite this

@inproceedings{ed8f46cf60e04b2f8853abeca8acb45e,

title = "A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol",

abstract = "This paper reports on the results of the application of formal methods in the development of an industrial, mission-critical system, called the Operator Support System. A critical communication protocol of this system, the OM/RR Protocol, and its corresponding service were formalised using the formal specification language Lotos. The resulting specifications have been validated using the tool set Lite and models of the specifications, obtained by making abstractions, have been verified using the tool Eucalyptus. Whereas the use of formal methods is usually motivated by their ability to allow for unambiguous and precise system descriptions amenable to mathematical reasoning, it turned out that in this project most benefits were obtained by the sheer process of formalising the informal protocol description, revealing many omissions and ambiguities. The results and experiences obtained during formalisation, validation, abstraction and verification are discussed on a non-formal basis in this paper.",

keywords = "FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS",

author = "Tim Willemse and Jan Tretmans and Arjen Klomp",

year = "2000",

language = "English",

series = "GMD Report",

publisher = "G.M.D.",

pages = "331--344",

editor = "Stefania Gnesi and Ina Schieferdecker and Axel Rennoch",

booktitle = "5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000",

note = "5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000, FMICS ; Conference date: 03-04-2000 Through 04-04-2000",

url = "https://fmics.inria.fr/workshop-5/",

}

Willemse, T, Tretmans, J & Klomp, A 2000, A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol. in S Gnesi, I Schieferdecker & A Rennoch (eds), 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000. GMD Report, vol. 91, G.M.D., pp. 331-344, 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000, Berlin, Germany, 3/04/00.

A Case Study in Formal Methods : Specification and Validation of the OM/RR Protocol. / Willemse, Tim; Tretmans, Jan; Klomp, Arjen.

5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000. ed. / Stefania Gnesi; Ina Schieferdecker; Axel Rennoch. G.M.D., 2000. p. 331-344 (GMD Report; Vol. 91).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Case Study in Formal Methods

T2 - 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000

AU - Willemse, Tim

AU - Tretmans, Jan

AU - Klomp, Arjen

N1 - Conference code: 5

PY - 2000

Y1 - 2000

N2 - This paper reports on the results of the application of formal methods in the development of an industrial, mission-critical system, called the Operator Support System. A critical communication protocol of this system, the OM/RR Protocol, and its corresponding service were formalised using the formal specification language Lotos. The resulting specifications have been validated using the tool set Lite and models of the specifications, obtained by making abstractions, have been verified using the tool Eucalyptus. Whereas the use of formal methods is usually motivated by their ability to allow for unambiguous and precise system descriptions amenable to mathematical reasoning, it turned out that in this project most benefits were obtained by the sheer process of formalising the informal protocol description, revealing many omissions and ambiguities. The results and experiences obtained during formalisation, validation, abstraction and verification are discussed on a non-formal basis in this paper.

AB - This paper reports on the results of the application of formal methods in the development of an industrial, mission-critical system, called the Operator Support System. A critical communication protocol of this system, the OM/RR Protocol, and its corresponding service were formalised using the formal specification language Lotos. The resulting specifications have been validated using the tool set Lite and models of the specifications, obtained by making abstractions, have been verified using the tool Eucalyptus. Whereas the use of formal methods is usually motivated by their ability to allow for unambiguous and precise system descriptions amenable to mathematical reasoning, it turned out that in this project most benefits were obtained by the sheer process of formalising the informal protocol description, revealing many omissions and ambiguities. The results and experiences obtained during formalisation, validation, abstraction and verification are discussed on a non-formal basis in this paper.

KW - FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

M3 - Conference contribution

T3 - GMD Report

SP - 331

EP - 344

BT - 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000

A2 - Gnesi, Stefania

A2 - Schieferdecker, Ina

A2 - Rennoch, Axel

PB - G.M.D.

Y2 - 3 April 2000 through 4 April 2000

ER -

A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol

Abstract

Publication series

Workshop

Keywords

Fingerprint

Cite this