Universität Bremen  
  FB 3  
  Group BKB > Teaching > SoSe 10 > Deutsch
English
 

Software specification in CASL

 
A course by Till Mossakowski at the Universität Bremen 2010.

03-05-H-706.54
Category A
Prerequisites: content of 600.01, 600.02, 601.01, 601.02, 604.02
ECTS: 6
Monday 12:00 - 14:00 MZH 4194,
Tuesday 12:00 - 14:00 MZH 1450

Start: Monday, April 12th

CASL, the Common Algebraic Specification Language, is an expressive language for the specification of software systems and other formal entities.

The most fundamental assumption is that programs are modelled as algebraic structures that include a collection of sets of data values together with functions over those sets. This level of abstraction is commensurate with the view that the correctness of the input/output behaviour of a program takes precedence over all its other properties. Another common element is that specifications of programs consist mainly of logical axioms, describing the properties that the functions are required to satisfy---often just by their interrelationship.

CASL consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications; the latter are used to prescribe the modular structure of implementations.

The course will give an introduction to CASL, discuss sample case studies and will also explain how to use analysis and verification tools (like the heterogeneous tool set and the automatic theorem prover SPASS) for CASL specifications. These can be used for finding errors (like inconsistencies) at an early phase, as well as for proving intended consequences of a specification. Finally, it is also possible to derive executable programs from (algorithmic) specifications.

Literature

Software

  • The heterogeneous tool set
    Local installation: /home/linux-bkb/bin/hets
  • The automatic theorem prover SPASS
    Local installation: /home/linux-bkb/bin/SPASS

Slides

 
   
Author: Dr. Till Mossakowski
 
  Group BKB 
Last updated: April 6, 2010   impressum