Specification styles in distributed systems design and verification

C.A. Vissers, Giuseppe Scollo, Marten J. van Sinderen, Hendrik Brinksma

    Research output: Contribution to journalArticleAcademicpeer-review

    81 Citations (Scopus)
    74 Downloads (Pure)

    Abstract

    Substantial experience with the use of formal specification languages in the design of distributed systems has shown that finding appropriate structures for formal specifications presents a serious, and often underestimated problem. Its solutions are of great importance for ensuring the quality of the various designs that need to be developed at different levels of abstraction along the design trajectory of a system. This paper introduces four specification styles that allow us to structure formal specifications in different ways: the monolithic, the constraint-oriented, the state-oriented, and the resource-oriented style. These styles have been selected on the basis of their suitability to express design concerns by structuring specifications and their suitability to pursue qualitative design principles such as generality, orthogonality, and open-endedness. By giving a running example, a query-answer service, in the ISO specification language LOTOS, these styles are discussed in detail. The support of verification and correctness preserving transformation by these styles is shown by verifying designs, expressed in different styles, with respect to each other. This verification is based on equational laws for (weak) bisimulation equivalence.
    Original languageUndefined
    Pages (from-to)179-206
    Number of pages28
    JournalTheoretical computer science
    Volume89
    Issue number1
    DOIs
    Publication statusPublished - Oct 1991

    Keywords

    • EWI-6878
    • CR-D.2.1
    • CR-F.3.1
    • METIS-118620
    • SCS-Services
    • IR-18101
    • CR-C.2

    Cite this