5th International Workshop on
Formal Methods for Industrial Critical Systems
Berlin, April 3-4, 2000
A Case Study in Formal Methods:
Specification and Validation of the
OM/RR Protocol
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 in this
paper.
Note: The content of the following files is part of
GMD Report No. 91
and subject to its copyright.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch