Do-CASL

an Observer-based CASL extension for Dynamic Specifications

DO-CASL is an extension to the CASL algebraic specification language. It is based on CASL-LTL and aims to provide a readable, compact and modular way of writing frame assumptions in loose specifications of complex dynamic systems.

Available resources

• A simple translator that converts well-formed DO-CASL without temporal logics to standard CASL.
• An example specification giving a loose specification of a P2P messaging infrastructure.
• A paper: Matteo Dell'Amico and Maura Cerioli, Injecting Distribution in CASL. Dagstuhl Seminar 05081 on Foundations of Global Computing. Dagstuhl, Germany, 20-25/02/2005.