Specification styles in distributed systems design and verification


Vissers, Chris A. and Scollo, Giuseppe and Sinderen, Marten van and Brinksma, Ed (1991) Specification styles in distributed systems design and verification. Theoretical computer science, 89 (1). pp. 179-206. ISSN 0304-3975

open access
PDF - Published Version
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.
Item Type:Article
Copyright:© 1991 Elsevier Science
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/18101
Official URL:https://doi.org/10.1016/0304-3975(90)90111-T
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 118620