Verifying Generative Casl Architectural Specifications
We present a proof-calculus for architectural specifications, complete w.r.t. their generative semantics. Architectural specifications, introduced in the Casl specification language, are a formal mechanism for expressing implementation steps in program development. They state that to implement a needed unit, one may implement some other units and then assemble them in the prescribed manner; thus they capture modular design steps in the development process. We focus on developing verification techniques applicable to full Casl architectural specifications, which involves, inter alia, getting around the lack of amalgamation in the Casl institution.
Unable to display preview. Download preview PDF.
- [CASL]Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P., Sannella, D., Tarlecki, A.: Casl: The Common Algebraic Specification Language. TCS (to appear)Google Scholar
- [CASL00]Casl – Summary and Semantics (note S-9), ver. 1.0. In: [CoFI] (2000)Google Scholar
- [CoFI]CoFI, The Common Framework Initiative for Algebraic Specification and Development. Documents accessible, at http://www.brics.dk/Projects/CoFI
- [Mos98]Mossakowski, T.: Cocompleteness of the Casl signature category. In: [CoFI], note S-7 (1998)Google Scholar
- [SMTKH]Schröder, L., Mossakowski, T., Tarlecki, A., Klin, B., Hoffman, P.: Amalgamation in the Semantics of Casl. TCS (to appear)Google Scholar