Specification styles in distributed systems design and verification

C.A. Vissers, G. Scollo, M.J. Sinderen, van, E. Brinksma

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

    81 Citaten (Scopus)
    1 Downloads (Pure)

    Samenvatting

    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.
    Originele taal-2Engels
    Pagina's (van-tot)179-206
    Aantal pagina's28
    TijdschriftTheoretical Computer Science
    Volume89
    Nummer van het tijdschrift1
    DOI's
    StatusGepubliceerd - 1991

    Vingerafdruk

    Duik in de onderzoeksthema's van 'Specification styles in distributed systems design and verification'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit