Name
Abstract | ||
|---|---|---|
CASL, a specification formalism developed recently by the CoFI group, offers architectural specifications as a way to describe how simpler modules can be used to construct more complex ones. The semantics for Casl architectural specifications formulates static amalgamation conditions as a prerequisite for such constructions to be well-formed. These are non-trivial in the presence of subsorts due to the failure of the amalgamation property for the Casl institution. We show that indeed the static amalgamation conditions for Casl are undecidable in general. However, we identify a number of practically relevant special cases where the problem becomes decidable and analyze its complexity there. In cases where the result turns out to be PSPACE-hard, we discuss further restrictions under which polynomial algorithms become available. All this underlies the static analysis as implemented in the Casl tool set. |
Year | Venue | Keywords |
|---|---|---|
2001 | MFCS | architectural specification,static amalgamation condition,amalgamation property,casl architectural specification,casl tool set,c asl architectural specifications,relevant special case,cofi group,checking amalgamability conditions,casl institution,polynomial algorithm,static analysis,decidability,algorithms |
Field | DocType | ISBN |
Discrete mathematics,Common Algebraic Specification Language,Programming language,Computer science,Static analysis,Formal specification,Decidability,Formalism (philosophy),Software architecture,Amalgamation property,Undecidable problem | Conference | 3-540-42496-2 |
Citations | PageRank | References |
8 | 0.58 | 4 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bartek Klin | 1 | 343 | 26.90 |
| Piotr Hoffman | 2 | 32 | 4.08 |
| Andrzej Tarlecki | 3 | 1514 | 124.61 |
| Lutz Schröder | 4 | 597 | 64.16 |
| Till Mossakowski | 5 | 1052 | 90.11 |