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

80 Citations (Scopus)
54 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

@article{f8c5ae52d217444ea9638b8e58bf594a,
title = "Specification styles in distributed systems design and verification",
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.",
keywords = "EWI-6878, CR-D.2.1, CR-F.3.1, METIS-118620, SCS-Services, IR-18101, CR-C.2",
author = "C.A. Vissers and Giuseppe Scollo and {van Sinderen}, {Marten J.} and Hendrik Brinksma",
year = "1991",
month = "10",
doi = "10.1016/0304-3975(90)90111-T",
language = "Undefined",
volume = "89",
pages = "179--206",
journal = "Theoretical computer science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1",

}

Specification styles in distributed systems design and verification. / Vissers, C.A.; Scollo, Giuseppe; van Sinderen, Marten J.; Brinksma, Hendrik.

In: Theoretical computer science, Vol. 89, No. 1, 10.1991, p. 179-206.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Specification styles in distributed systems design and verification

AU - Vissers, C.A.

AU - Scollo, Giuseppe

AU - van Sinderen, Marten J.

AU - Brinksma, Hendrik

PY - 1991/10

Y1 - 1991/10

N2 - 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.

AB - 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.

KW - EWI-6878

KW - CR-D.2.1

KW - CR-F.3.1

KW - METIS-118620

KW - SCS-Services

KW - IR-18101

KW - CR-C.2

U2 - 10.1016/0304-3975(90)90111-T

DO - 10.1016/0304-3975(90)90111-T

M3 - Article

VL - 89

SP - 179

EP - 206

JO - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

IS - 1

ER -