## 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.

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.

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

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.

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

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

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.

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

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.

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".)

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.

Excursion to the Gower.

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.

Group Meeting: Teme gives the presentation "Specifying a Remote Control in CSP-CASL".

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

Gift, Liam, Markus and Teme attended BCTCS 2007 in Oxford, where Gift, Liam and Teme made presentations.

Gift, Liam and Teme present final test talks in preparation for BCTCS 2007.

Gift and Liam present test talks in preparation for BCTCS 2007.

Markus attends a meeting of the IFIP WG 1.3 and gives a presentation on CSP-Prover.

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

Group Meeting: Andy gives the presentation "Natural Semantics".

Temesghen gives the talk "A Glimpse of Category Theory" in the No Grownups Seminar.

Group Meeting.

Group Meeting.

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

Group Meeting: Gift gives the presentation "Stable Revivals Model and Implementation in CSP".

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

Group Meeting: Markus gives the presentation "Structured Specifications".

Group Meeting: Andy and Liam give the presentation "Introduction to HETS (the Heterogeneous Tool Set)".

Group Meeting: Markus gives the presentation "How to Cook Up a Presentation".

Group Meeting: Markus gives the presentation "Sub-sorting in CASL".

Group Meeting: Markus gives the presentation "Operational, Denotational, and Axiomatic CSP Semantics".

Group Meeting: Markus gives the presentation "Complete Partial Orders in the CSP Setting".

Group Meeting.

Group Meeting: Holger gives the presentation "Introduction to Temporal Logic".

Temesghen gives a presentation in the Swansea Algebraic Specification Seminar on MSc thesis. Title: "Towards Semi Automated Equivalence Checking of Spi Calculus Processes".

Gift gives the talk "Model Checking Live Sequence Charts (A Report on the paper)" in the No Grownups Seminar.

Trip to Gregynog, Where the postdoctoral students of the group made presentations on the 20.11.06. The presentations were as follows :-

- Andy - Parsing CSP-CASL with Parsec.
- Gift - CSP Laws and How to Prove the Correctness in CSP-Prover.
- Liam - Various Logics Fit into the Framework of an Algebraic Logic.
- Temesghen - Refinement notions in CSP and Algebraic Specification.

Group Meeting: Liam gives the presentation "A Monadic Parser in Haskell".

Group Meeting: Temesghen gives the presentation "How to Write a Proof".

Group Meeting: Andy gives the presentation "Parser II".

Markus dressed up for an Awards Ceremony, Teme as usual :-)

Group Meeting: Andy gives the presentation "Parser I".

Group Meeting: Markus gives the presentation "Categories II".

Group Meeting: Markus gives the presentation "Categories I".

Group Meeting: Gift gives the presentation "Sequential Processes".

Markus gives a presentation in the Swansea Algebraic Specification Seminar on "CSP-CASL: Semantics, Application, Tools".

Official birth of the group.

Temesghen arrives.

Markus participates at AVoCS 06.

Yoshinao Isobe gives a presentation in the Swansea Algebraic Specification Seminar on a complete axiomatic semantics for the CSP stable-failures model.

Liam arrives.

Group Meeting: Markus gives the presentation "Recursion in CSP".

Group Meeting: Markus gives the presentation "Overview on CSP".

Yoshinao Isobe visits Swansea.

Presentation of "A Complete Axiomatic Semantics for the CSP Stable-Failures Model" at CONCUR 2006.

EPSRC project starts.

Gift arrives.