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
and your browser is able to play WAV sound samples (16 bits,
mono, 11,025 Hz), just click, listen, and enjoy.
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).
slurped 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.
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:
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.''
In the afternoon, we went to Seili Island on a
boat called ``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.
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:
electronic (one guy with a computer, one girl
singing)
pop (the song title is ``This is how I
am'')
Jazz
Later we went to a pub (``Erik Public House'') and to a disco (``Puuteri'').
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!
And 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 this 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.
In the evening, we had dinner at a restaurant called ``Herman'', which was
somewhat exclusive; even an annoying piano player
was present.
rain. 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
``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 beeps of the traffics
lights.
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.
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''.
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 medieval music.
In the evening we added ``Dynamo'', ``Amarillo'', and ``Opera'' to our set of known pubs and discos.
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.
sound 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 traditional 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 toilet 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.
