Observational interpretation of Casl specifications

We explore the way in which the refinement of individual ‘local’ components of a specification relates to the development of a ‘global’ system from a specification of requirements. The observational interpretation of specifications and refinements adds expressive power and flexibility, but introduce...

Full description

Saved in:
Bibliographic Details
Published in:Mathematical structures in computer science 2008-04, Vol.18 (2), p.325-371
Main Authors: BIDOIT, MICHEL, SANNELLA, DONALD, TARLECKI, ANDRZEJ
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We explore the way in which the refinement of individual ‘local’ components of a specification relates to the development of a ‘global’ system from a specification of requirements. The observational interpretation of specifications and refinements adds expressive power and flexibility, but introduces some subtle problems. Our study of these issues is carried out in the context of Casl architectural specifications. We introduce a definition of observational equivalence for Casl models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.
ISSN:0960-1295
1469-8072
DOI:10.1017/S0960129507006536