This is the English version. A German version is available also.
Dies ist die englische Version. Eine deutsche Version ist auch vorhanden.

Version: 1.07

Travelogue

Summer School on Specification, Refinement, and Verification in Turku, Finland, August 9-22, 1998

Abstract. This document is a log of the adventures of three students from Kiel, Germany, during their visit of the Summer School on Specification, Refinement, and Verification in Turku, Finland, in August 1998. Kai Baukus, Ben Lukoschus, and Karsten Stahl are the heroes of this story.
This work is structured as follows: We start with the lists of lecturers and participants, which have been moved to linked appendices for the sake of readability. An extensive description of all interesting events will be given in chronological order in the main part. We conclude with some questions to the interested reader.

List of Lecturers
List of Participants

Have a look at the photos taken by Clara María Segura Díaz!

Technical note. Since I was equipped with a portable MiniDisc recorder, I was able to collect loads of different sounds during the stay in Finland. So whenever you come across the microphone icon sound sample and your browser is able to play WAV sound samples (16 bits, mono, 11,025 Hz), just click, listen, and enjoy.

Sunday, August 9, 1998

We left Kiel by bus to get to Hamburg airport. Checking in went fine, and the lady at the luggage counter wished us ``a nice holiday.'' The Iberia Airlines plane number IB 6942 came from Madrid and continued its flight to Helsinki. During the flight, we had a beautiful view on the Baltic Sea.

In Helsinki we had to take a train to Turku, but we did not know that the railway station was about 20 kilometers away. So we took a Finnair bus to the station, and we arrived just in time for our train, two minutes before it was leaving.

Checking in at Hotel Centro was done quickly. Karsten and Ben shared a room, and Kai had two weeks to accustom himself to Holger from Münster.

We rounded off the evening by visiting McDonald's, where we were quite impressed about the length of Finnish words for such simple things like, e.g., ``fries'' (ranskalaiset perunat).

Monday, August 10, 1998

This morning, like every morning, started with a huge breakfast in the ``Scandinavian buffet'' style. For anyone who was able to eat lots of food very early in the morning this was like paradise. But some of us just sound sampleslurped some cups of coffee, tea, or hot chocolate.

After breakfast, a 20-minute walk took us to the Mauno Koivisto Center at the Turku Technology Center. A sophisticated ``traffic light timing strategy'' enabled us to spend as much time as possible at the breakfast table and as less time as possible on the roads of Turku.

Equipped with lots of papers, schedules, and beautiful high-quality name tags, we enjoyed a nice introduction to Finland, Turku, and its two universities, University of Turku and Åbo Akademi. After that, Orna Grumberg talked about Computer-aided verification of hardware and software.

The first coffee break turned out to be a coffee/tea/cake break, but the cakes surprisingly turned out to be liver patés. The next session was Refinement and verification techniques used in security by Martín Abadi, who talked about cryptography and protocols, and in a practical demonstration he showed that his transparencies are waterproof.

Then we had lunch at the Amica restaurant just a few steps down the hallway. The most interesting part of the meal was a strange drink called ``home beer'', which is some kind of partly processed beer with a taste somewhere between champagne and coke, or something completely different. We even did not dare to call this stuff ``liquid'', so the notion ``substance'' was introduced and used for that.

After lunch, Ralph-Johan R. Back talked about states, agents, and contracts in his Refinement calculus overview. The reference to his new book became a running gag for the next two weeks, and whenever there was a mistake discovered in the lecture, it was pointed out that ``it's okay in the book''.

In the evening we visited the Aboa Vetus & Ars Nova museums. The Aboa Vetus (Latin for ``old Turku'') museum shows medieval streets, houses, and cellars of over 700 years of Turku's history. Interesting pieces of 20th century art are shown in the Ars Nova (``new art'') museum. We concluded the visit with a buffet and beverages at the Café Niki inside the museum.

After another beer, respectively, coke, at ``Pappa Joe's Self-Service Banana Bar'' on a boat in the Aurajoki river, we went back to the hotel and played cards until we were tired enough to go to bed.

Tuesday, August 11, 1998

At breakfast, we overheard someone regretting that he used a radio alarm clock to wake up:
``Ricky Martin's song won't go out of my head for the whole day. That's the price you have to pay for being wakened up that way.''

The lectures of this day were Orna Grumberg's second part CTL model checking, Pamela Zave's talk about Specification and verification of telecommunication lines; Reino Kurki-Suonio presented an Incremental specification in a TLA-based approach to object systems, and Ralph-Johan R. Back continued his yesterday's talk. Some quotes represent the highlights of the lectures:

[If you missed the point in the first quote, your taste is probably not as bad as mine is. :-]

In the evening quite a large group went to the pizzeria ``Dennis''. The pizzas were very good, but I stupidly ordered lasagne, which wasn't good at all. I don't know if the beer tasted good, but Koen used this formulation when paying his bill: ``I had ravioli and a beer thing.''

Wednesday, August 12, 1998

On this day, there were only two lectures; Orna Grumberg and Reino Kurki-Suonio continued their talks.

In the afternoon, we went to Seili Island on a boat called sound sample``Watercat'' (not ``Watergate''). During the trip we had an amazing view on thousands of small islands scattered around, which is very typical for many Scandinavian coasts. And there was an attack of flying ants, something which you really don't expect when you are at sea.

Seili Island was first used as the location for a hospital for lepers, then for a lunatic asylum, and nowadays the university's Archipelago Research Institute is located there. (Look for more details here.) Ralph-Johan R. Back rang a huge bell next to a beautiful wooden church, upsetting the guide who told us that the bell is used as a fire bell only.

The strangest thing about Turku is the chimney of the local electricity company building. Going down from the top of the chimney, large, red neon light figures show the following numbers: 1  1  2  3  5  8  13  21  34  55, which is the beginning of the Fibonacci sequence.

Thursday, August 13, 1998

In the morning sessions, Pamela Zave continued her talk about the AT&T telephone features, and Martín Abadi presented the pi calculus for security protocols. Some quotes of his talk:

And if you ever meet Martín Abadi in person, ask him about the ``wide mouth frog joke''.

After lunch, Eric C.R. Hehner started with A practical theory of programming. Since Martin Büchi (the official summer school photographer) tried to get a good angle for taking a picture of him for quite some time, Eric said: ``Can you hurry up and go `click'?''

The last session of the day was Orna Grumberg's last lecture, which she concluded with an overview of model checking and theorem proving tools.

This night was the ``Night of the Arts'', and among other things we listened to some bands playing various kinds of music:

Later we went to a pub (``Erik Public House'') and to a disco (``Puuteri'').

Friday, August 14, 1998

Martín Abadi started this morning with A type system for the Java virtual machine, and he soon recognized that many of us were not quite awake:
``So how many of you know Java? And how many went to a disco last night?--So I should go a bit slower.''

Pamela Zave and Eric C.R. Hehner continued their talks. The latter mentioned the Data Refinement Book by Willem-Paul de Roever and Kai Engelhardt during his talk (actually, Eric did not know the second author's name and said ``some other guy''). Why do I mention this book? Well, it was written at our university in Kiel, so go and buy it! :-)

At 15:30, there was this session called ``Questions I'', were the participants had the possibility to ask questions about the lectures of the first week. Since initially nobody dared to ask something, one of the lecturers started with a quite large question about open and closed systems:

Eric C.R. Hehner: ``So you wanna say that if the environment behaves in a certain way then the system behaves in a certain way. And in a sense that looks like I have to describe the environment as well as describing the system. But it's not true! I'm not saying what the environment does. I'm saying if the environment does this, then the system does that. I also have to say what the environment does. Maybe it does exactly that; in which case I get the behavior I want. But maybe it doesn't, maybe the environment does something else. In which case, in order to show that I get the behavior I want, I now gonna have some additional proof obligation. [...]
But the point is: This is a description of the system, not of the environment, although of course it makes assumptions about the environment, and this a description of the environment. And you don't want to describe a closed system, 'cause a closed system does nothing! Something that doesn't react with its environment does nothing!
sound sampleAnd the question is ... what do you think of that?''

Reino Kurki-Suonio: ``You said that a closed system does nothing. It certainly does, if you are able to observe some of the variables that are modified [...]''

Martín Abadi: ``It's a closed system with a window.''

Eric C.R. Hehner: ``With a window ... well, I think that a window is being an interaction with the environment, of course it's an interaction in the outward direction, but nevertheless an interaction with the environment.''

Reino Kurki-Suonio: ``Okay, it sounds to me that this is just a viewpoint how you want to deal with this. So to me a closed system certainly does modify variables that I can look at through the window, and moreover, that closed system given this window gives me the possibility of superposing something that can use these variables somehow. And if I do these superpositions correctly so that I do preserve also liveness properties then I get a sort of closed system plus an interacting observer. So it is a possibility of adding something more, sort of another environment by superposition.''

After this discussion there were some questions from the audience, like sound samplethis one concerning two of Eric C.R. Hehner's obscure proof tricks:

Koen Claessen: ``So you showed two dubious things, ...''
Eric C.R. Hehner: ``Yes.''
Koen Claessen: ``...and you're not going to explain any more about why you think these dubious things are correct?''
Eric C.R. Hehner (after a long pause): ``No.''

Another important issue were the ``angels & demons'', which had been introduced by Ralph-Johan R. Back:

Reino Kurki-Suonio: ``From your transparencies I know that users are female. But I never judged whether angels & demons are.''
Ralph-Johan R. Back:``I won't answer that question. I have an opinion, but I won't say it.''

This day's social evening was a visit to Villa Y-Hovi in Ruissalo, where we had an evening meal, and then we went into the famous Finnish Sauna. The temperature difference between the sauna (90 °C) and the Baltic Sea (17 °C) was very refreshing, and everyone had much fun.

Michel Sintzoff to Eric C.R. Hehner: ``You look like a lobster.''

At 23:00, we went back to the hotel, and immediately started off to the ``Puuteri'', were we stayed until they closed at about 4 o'clock. On our way back, we met a completely drunk woman named Mira, who was sitting in the middle of the street. As she realized that some of us came from Germany, she told us at least five times that she had been to Germany with her parents when she was a young girl. And she had also been to a sauna there. We let her talk for about twenty minutes. Then we left.

Saturday, August 15, 1998

Weekend. We got up as late as possible (the end of the hotel's breakfast time was a hard deadline). After breakfast, we went shopping. Two large groups made a bicycle trip, but we did not trust the weather and stayed in the hotel, playing cards the whole day long.

In the evening, we had dinner at a restaurant called ``Herman'', which was somewhat exclusive; even an sound sampleannoying piano player was present.

Sunday, August 16, 1998

Sunday morning started with neverending Finnish sound samplerain. We had the honor of sharing our breakfast table with Martín Abadi, who was leaving Finland on that day.

In the afternoon, is was still raining, so we watched the Formula 1 Grand Prix in Hungary on Finnish television. While Mika Häkkinen had trouble with his McLaren Mercedes, the Ferrari of his rival Michael Schumacher worked well, and sound sample``Schumi'' was able to win the race.

We had dinner at the ``Ribs'' restaurant. On our way back to the hotel we collected another Finnish sound, the annoying sound samplebeeps of the traffics lights.

Monday, August 17, 1998

This morning Kaisa Sere talked about Action systems--a state-based formalism for distributed computing. Eric C.R. Hehner, who continued his talk with a focus on concurrency, detected the real problem of the ``dining philosophers'':
``I don't know how to eat spaghetti with two forks.''

In the afternoon, we listened to Ralph-Johan R. Back and to Amir Pnueli's lecture Verification of reactive systems. He told us about the story behind Leslie Lamport's acronym ``TLA''. ``TLA'' stands for ``three letter acronym'', showing that the most important thing when introducing something new is a name that can be abbreviated to three letters.

Tuesday, August 18, 1998

Nothing much happened in the lectures, except that we had to use a different room for the lectures of Kaisa Sere and Amir Pnueli, since the president of Tanzania, Benjamin Mkapa, needed the room at the Mauno Koivisto Center for a press conference.

In the afternoon we had a look at the Bonk Inc. museum in Uusikaupunki and had dinner at the Kala-Trappi restaurant in Naantali. Finally, we made a pub tour, visiting the ``Old Pharmacy'', ``Erik'', ``Café Noir'', and the ``57''.

Wednesday, August 19, 1998

Another day full of lectures. Jean-Raymond Abrial started with Logic, proofs and provers. Then Ralph-Johan R. Back had his last lecture. Amir Pnueli talked about Symbolic model checking, and Eric C.R. Hehner presented a way to go From Boolean algebra to unified algebra. Some quotes of this day:

Thursday, August 20, 1998

Three more lectures, the second of Jean-Raymond Abrial, a new one by Joakim von Wright, Program refinement and theorem proving: modeling and tool support, and Amir Pnueli's last lecture.

In the afternoon we visited Turku Castle and learned much about the history of Turku and life in the middle ages; and now we know why spiral staircases were build in clockwise direction. We had dinner at the castle's Juhana Herttuan Kellari, where we enjoyed good food and a speech of Amir Pnueli, and we listened to some sound samplemedieval music.

In the evening we added ``Dynamo'', ``Amarillo'', and ``Opera'' to our set of known pubs and discos.

Friday, August 21, 1998

Bad luck on this day: It was raining during our walk to the university. Thus, we got quite wet. While drying, we enjoyed the last lectures of Jean-Raymond Abrial and Joakim von Wright.

In the evening, a large group met for a final drink at the ``Old School'', and some time later went on to the ``Amarillo''. Since we had to get up quite early, we did not stay that long.

Saturday, August 22, 1998

After breakfast, we checked out at 8:15 in the morning. On our way to the railway station, the rolling suitcases made a nice sound samplesound on the pavement. In the train to Helsinki we were accompanied by two Dutch guys (Victor Bos and Martijn Oostdijk), and we joined again later to take the bus to Helsinki airport.

In Helsinki we had some hours to look at the city before our plane left for Hamburg. So we walked around a bit and listened to some sound sampletraditional Finnish music. We had lunch at the Planet Hollywood restaurant, were we had some decent but a bit expensive hamburgers. The definitive aural highlight of this travelogue is of course the sound sampletoilet flush in the men's room at Planet Hollywood Helsinki.

At the airport we again saw some familiar faces, before we boarded our flight IB 6943 to Hamburg. By the way: If you really want to understand the public announcements at airports, you should go to the toilet, where there is a much better acoustics.

In Hamburg, we only had 13 minutes to fetch our luggage before the bus was leaving for Kiel. Somehow we made it.

Questions

Did you know that ...
DISCLAIMER: This document has been written for private, non-profit entertainment purposes only. If you feel offended in any way by anything found here, I apologize for overestimating your sense of humor, and I will immediately remove the offensive parts.
Ben Lukoschus  (ben@lukoschus.de)
Last modified: 2003-06-26 14:27:19 CEST (+0200)