Property preserving development and testing for Csp-Casl

Photograph of Temesghen Kahsai

Temesghen Kahsai


The time has come to tell you a little bit about what I did in the
last three years sitting in my cubical (apart from drinking coffee and
playing Labminton). Basically, I will give an overview of the results
described in my PhD thesis.

In this talk I will illustrate some development notions for the
specification language Csp-Casl. Such notions are capable of
capturing informal vertical and horizontal software developments
which we typically find in industrial applications (e.g. electronic
payment system). On the other hand, such development notions allow us
to verify some interesting properties, e.g., deadlock freedom.

I will also present a theory for the evaluation of test cases with
respect to Csp-Casl specifications. With this approach, it is possible
to develop test cases for even the most abstract and basic
specifications, and to reuse them later on in more refined systems.

The presented theoretical results have been applied to the electronic
payment system EP2. Here, I have modeled the system in Csp-Casl and
verified properties using tool support. Finally I will present a
hardware-in-the-loop testing framework for EP2. For the latter, I will
give a concrete demo with a 'real' payment terminal.

Tuesday 23rd February 2010, 14:00
Robert Recorde Room
Department of Computer Science