Swansea University
Computer Science

EPSRC Project EP/D037212/1

Diary

Year 1: 01.08.2006 - 31.07.2007


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.

Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa Photo from Markus' trip to the University of Pretoria, South Africa


15.06.07 - 25.06.07

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.

Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin Photo from Temesghen's and Markus' trip to Berlin


13.06.07

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


06.06.07

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


24.05.07 - 25.05.07

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.

Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home Photo from the dinner party at Markus' Home

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.

Photo from José Luiz Fiadeiro talk Photo from José Luiz Fiadeiro talk Photo from José Luiz Fiadeiro talk Photo from José Luiz Fiadeiro talk Photo from José Luiz Fiadeiro talk Photo from José Luiz Fiadeiro talk


23.05.07

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


23.05.07

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


16.05.07

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

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

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

Excursion to the Gower.

Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea Photo from our excursion to the Gower in Swansea


02.05.07

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.


25.04.07

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.


02.04.07 - 05.04.07

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

Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford Photo from our trip to BCTCS 2007 in Oxford


29.03.07

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


27.03.07

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



23-24.03.07

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


21.03.07

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.


14.03.07

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


09.03.07

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


28.02.07

Group Meeting.


21.02.07

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.


14.02.07

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.


07.02.07

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


05.02.07

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


25.01.07

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


18.01.07

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


11.01.07

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


14.12.06

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


07.12.06

Group Meeting.


30.11.06

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


24.11.06 - 3.12.06

Holger visits Swansea for a course on Testing.


24.11.06

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


19.11.06 - 22.11.06

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

Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog Photo from Gregynog


09.11.06

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


09.11.06

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


03.11.06

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


01.11.06

Markus and Temesghen

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


26.10.06

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


19.10.06

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


12.10.06

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


05.10.06

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


28.09.2006

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


22.09.2006

Official birth of the group.


20.09.2006

Temesghen arrives.


18.09.2006 - 19.09.2006

Markus participates at AVoCS 06.


12.09.2006

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


11.09.2006

Liam arrives.

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


04.09.06

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


03.09.2006 - 14.09.2006

Yoshinao Isobe visits Swansea.


27.08.2006

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


01.08.2006

EPSRC project starts.

Gift arrives.