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 proceedingConference contributionAcademicpeer-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 languageEnglish
    Title of host publication5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
    EditorsStefania Gnesi, Ina Schieferdecker, Axel Rennoch
    PublisherG.M.D.
    Pages331-344
    Number of pages14
    Publication statusPublished - 2000
    Event5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000 - Berlin, Germany
    Duration: 3 Apr 20004 Apr 2000
    Conference number: 5
    https://fmics.inria.fr/workshop-5/

    Publication series

    NameGMD Report
    PublisherGMD
    Volume91
    ISSN (Print)1435-2702

    Workshop

    Workshop5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
    Abbreviated titleFMICS
    Country/TerritoryGermany
    CityBerlin
    Period3/04/004/04/00
    Internet address

    Keywords

    • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

    Fingerprint

    Dive into the research topics of 'A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol'. Together they form a unique fingerprint.

    Cite this