by Lutz Schröder, Till Mossakowski, Andrzej Tarlecki, Piotr Hoffman and Bartek Klin
Abstract:
We present a semantics for architectural specifications in CASL, including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for CASL models. To circumvent this problem, we extend the CASL logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Moreover, amalgamation for enriched CASL means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for CASL.
Reference:
Lutz Schröder, Till Mossakowski, Andrzej Tarlecki, Piotr Hoffman and Bartek Klin: Amalgamation in the semantics of CASL, In Theoretical Computer Science, 331(1), pp. 215–247, 2005. [preprint]
Bibtex Entry:
@Article{SchroderEA04,
author = {Lutz Schr{\"o}der and Till Mossakowski and Andrzej Tarlecki and Piotr Hoffman and Bartek Klin},
title = {Amalgamation in the semantics of {CASL}},
year = {2005},
journal = {Theoretical Computer Science},
volume = {331},
pages = {215-247},
number = {1},
keywords = {amalgamation CASL semantics architectural structural specification enriched},
url = {http://dx.doi.org/10.1016/j.tcs.2004.09.037},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/amalg.pdf"> [preprint] </a>},
psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/amalg.ps},
abstract = {We present a semantics for architectural specifications in CASL,
including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for CASL models. To circumvent this problem, we extend the CASL logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Moreover, amalgamation for enriched CASL means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for CASL.
},
issn = {0304-3975},
}