Diary Year 1: 01.08.2006 - 31.07.2007

Error message

Deprecated function: The each() function is deprecated. This message will be suppressed on further calls in menu_set_active_trail() (line 2375 of /compsci/partition2/csmarkus/public_html/ProcessesAndData/includes/menu.inc).
Deprecated function: Methods with the same name as their class will not be constructors in a future version of PHP; views_display has a deprecated constructor in require_once() (line 3062 of /compsci/partition2/csmarkus/public_html/ProcessesAndData/includes/bootstrap.inc).
Deprecated function: Methods with the same name as their class will not be constructors in a future version of PHP; views_many_to_one_helper has a deprecated constructor in require_once() (line 113 of /compsci/partition2/csmarkus/public_html/ProcessesAndData/sites/all/modules/ctools/ctools.module).

31.07.2007 - 12.08.2007

Temesghen attends the international summer school Marktoberdorf 2007 and gives a talk on "Specification Based Testing for Refinement". Below are some pictures from the trip.

27.07.2007

Temesghen's progression meeting with Ben Mora, Uli Berger, and Markus Roggenbach as representatives.

01.07.2007 - 15.07.2007

Markus visits Derrick Kourie and Stefan Gruner at the University of Pretoria, South Africa as part of a South-Africa-UK-Network funded by the National Research Foundation and the Royal Society. Whilst there Markus takes a seminar on CSP-Prover. Below are some Photos from the trip.

Temesghen and Markus visit Fraunhofer Institute FIRST, Berlin. As part of the Erasmus teaching staff exchange between Humboldt University (Berlin) and Swansea University (Wales), Markus taught over two weekends the course "Algebraic Specification for Hardware and Software" to graduate students.

Markus also gave a talk about CSP-Prover in the Ringvorlesung at the Department of Computer Science at Humboldt University, Berlin. Below are some photos from the trip, showing Markus, Holger and Temesghen participating in various activates whilst at Berlin.

13.06.2007

Group Meeting: Exercise - "Specifying A Medical Monitoring Device".

06.06.2007

Group Meeting: Open discussion - "Specifying Elevators with CSP-CASL - Part 5" (Final Part).

24.05.2007 - 25.05.2007

José Luiz Fiadeiro visits to make a presentation in the Swansea Algebraic Specification Seminar.

Markus hosted an informal dinner party at his home to welcome José, there was good food, nice company and very nice cocktails from our resident bar man, Temesghen. Photos of this great evening are below. José also gave our group a small talk on "The Social Life of Categories", which complemented our Hauptseminar on Category Theory. Some photos from both talks are below.

23.05.2007

Group Meeting: Open discussion - "Specifying Elevators with CSP-CASL - Part 4".

16.05.2007

Group Meeting: Open discussion - "Specifying Elevators with CSP-CASL - Part 3".

Liam made the presentation "Institutions - Part 2" in the Hauptseminar. The Hauptseminar (2006/2007) has been a seminar designed to teach everyone Category Theory.

11.05.2007

Andy gives the talk "A pragmatic look at monads in Haskell" in the No Grownups Seminar. (Within an hour or two of publishing this, it was pointed out to me that this talk is really about the IO monad rather than monads in general, and that in particular the assertion that a monad represents a computation which performs a side-effect is not, in general true. A nice example is the Maybe monad. So a better title for this talk is "A pragmatic look at monadic I/O in Haskell".)

09.05.2007

Group Meeting: Open discussion - "Specifying Elevators with CSP-CASL - Part 2".

Liam made the presentation "Institutions - Part 1" in the Hauptseminar. The Hauptseminar (2006/2007) has been a seminar designed to teach everyone Category Theory.

02.05.2007

Excursion to the Gower.

02.05.2007

Group Meeting: Open discussion - "Specifying Elevators with CSP-CASL". We are going to try and use the language of CSP-CASL to specify a complex system (A system of elevator), by starting with an informal, natural language specification of an elevator controller. The specification follows.

An elevator control
The controller is responsible for n ≤ 8 elevators (called cars) serving m ≤ 256 floors. At each floor, there are two call buttons (up and down). (At the first floor, there is no down button and at floor m there is no up button, but this is irrelevant). Within each car there are m destination buttons. For each elevator the controller can issue a command to travel to a certain floor. In response, each car reports to the controller when it reaches a certain floor. The basic use case is: An actor wants to travel with a car. S/He pushes a call button, waits for a car, enters the car, pushes a destination button, travels to destination and leaves the car. (Remark: with a "real" elevator control, there are approximately 600 (!!) more use cases to be considered) The functionality of the controller in this case is: Whenever it receives a floor call, it determines a suitable car for this call. It then sends a car to the passenger. When the passenger pushes a destination button, it sends this car to the destination. For sake of simplicity, we can omit in-between stops for picking up other passengers. However, we have to consider that several passengers enter which want to travel to different destinations. Additionally, when there are no pending calls the controller can decide to send cars to certain parking positions; this is important for saving energy.