Verifying Generative Casl Architectural Specifications

  • Piotr Hoffman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)


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.

Unable to display preview. Download preview PDF.


  1. [BCH99]
    Bidoit, M., Cengarle, M.V., Hennicker, R.: Proof Systems for Structured Specifications and Their Refinements. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) Algebraic Foundations of Systems Specification, pp. 385–434. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. [Borz98]
    Borzyszkowski, T.: Completeness of a logical system for structured specifications. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 107–121. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. [BST99]
    Bidoit, M., Sannella, D., Tarlecki, A.: Architectural Specifications in Casl. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 341–357. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. [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
  5. [CASL00]
    Casl – Summary and Semantics (note S-9), ver. 1.0. In: [CoFI] (2000)Google Scholar
  6. [CoFI]
    CoFI, The Common Framework Initiative for Algebraic Specification and Development. Documents accessible, at
  7. [GB84]
    Goguen, J., Burstall, R.: Some fundamental algebraic tools for the semantics of computation. Part 1: Comma categories, colimits, signatures, and theories. TCS 31(2), 175–209 (1984)zbMATHGoogle Scholar
  8. [GB92]
    Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. Journal of the ACM 39, 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  9. [Hof01]
    Hoffman, P.: Verifying Architectural Specifications. In: Cerioli, M., Reggio, G. (eds.) WADT 2001 and CoFI WG Meeting 2001. LNCS, vol. 2267, pp. 152–175. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. [MAH01]
    Mossakowski, T., Autexier, S., Hutter, D.: Extending Development Graphs With Hiding. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 269–283. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. [Mos98]
    Mossakowski, T.: Cocompleteness of the Casl signature category. In: [CoFI], note S-7 (1998)Google Scholar
  12. [Pau96]
    Paulson, L.: ML for the Working Programmer. Cambridge Univ. Press, Cambridge (1991)zbMATHGoogle Scholar
  13. [SMT01]
    Schröder, L., Mossakowski, T., Tarlecki, A.: Amalgamation in Casl via Enriched Signatures. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 993–1004. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. [SMTKH01]
    Schröder, L., Mossakowski, T., Tarlecki, A., Klin, B., Hoffman, P.: Semantics of Architectural Specifications in Casl. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 253–268. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. [SMTKH]
    Schröder, L., Mossakowski, T., Tarlecki, A., Klin, B., Hoffman, P.: Amalgamation in the Semantics of Casl. TCS (to appear)Google Scholar
  16. [ST88]
    Sannella, D., Tarlecki, A.: Specifications in an Arbitrary Institution. Information and Computation 76(2/3), 165–210 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  17. [ST97]
    Sannella, D., Tarlecki, A.: Essential Concepts of Algebraic Specification and Program Development. Formal Aspects of Computing 9, 229–269 (1997)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Piotr Hoffman
    • 1
  1. 1.Institute of InformaticsWarsaw UniversityWarszawaPoland

Personalised recommendations