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 |
Keywords
- FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS