DO-Casl: An Observer-Based Casl Extension for Dynamic Specifications

  • Matteo Dell’Amico
  • Maura Cerioli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4019)


We present DO-Casl, a new member of the CASL family of specification languages. It is an extension of Casl-Ltl and it supports a methodology for conveniently writing loose specifications of observers on dynamic sorts. The need for such constructs arose during the development of a CASL library for distributed systems. Indeed, we have frequently used the same pattern of specification, in order to solve a generalization of the frame problem while using observers. The constructs we propose make the resulting specifications more readable, concise and maintainable. The semantics of our extension is given by reduction to standard Casl-Ltl, which is, in turn, reducible to standard Casl whenever temporal logic is not used. A small prototype of the pre-processor from DO-Casl to Casl-Ltl has been implemented as well.


Temporal Logic Label Transition System Frame Problem Concrete Syntax Observational Approach 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    CoFI (The Common Framework Initiative). In: Mosses, P.D. (ed.) CASL Reference Manual. LNCS (IFIP Series), vol. 2960, Springer, Heidelberg (2004)Google Scholar
  2. 2.
    Schröder, L., Mossakowski, T.: HasCasl: Towards integrated specification and development of Haskell programs. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 99–116. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Baumeister, H., Zamulin, A.V.: State-based extension of Casl. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 3–24. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Reggio, G., Astesiano, E., Choppy, C.: Casl-Ltl: A Casl extension for dynamic reactive systems – Version 1.0 – Summary. Technical Report DISI-TR-03-36, Univ. of Genova (2003)Google Scholar
  5. 5.
    Costa, G., Reggio, G.: Specification of abstract dynamic-data types: A temporal logic approach. TCS 173(2), 513–554 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Reichel, H.: Behavioural equivalence — a unifying concept for initial and final specification methods. In: Proc. 3rd. Hungarian CS Conference, pp. 27–39 (1981)Google Scholar
  7. 7.
    Cerioli, M.: Basic concepts. In: Algebraic System Specification and Development: Survey and Annotated Bibliography, 2nd edn. Monographs of the Bremen Institute of Safe Systems, vol. 3, Shaker, 1997 (1998)Google Scholar
  8. 8.
    Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21(10), 785–798 (1995)CrossRefGoogle Scholar
  9. 9.
    Choppy, C., Reggio, G.: Using Casl to specify the requirements and the design: A problem specific approach. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 104–123. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Cerioli, M., Mossakowski, T., Reichel, H.: From total equational to partial first-order logic. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) Algebraic Foundations of Systems Specification. IFIP State-of-the-Art Reports, Springer, Heidelberg (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Matteo Dell’Amico
    • 1
  • Maura Cerioli
    • 1
  1. 1.DISI–Dipartimento di Informatica e Scienze dell’InformazioneUniversità di GenovaGenovaItaly

Personalised recommendations