Summer School on Specification, Refinement, and Verification in Turku, Finnland, 9.-22. August 1998
Zusammenfassung.
Dieses Dokument ist ein Logbuch der Abenteuer von drei Studenten aus
Kiel, Deutschland, die sie beim Besuch der Summer School on
Specification, Refinement, and Verification in Turku, Finnland, in
August 1998 erlebt haben.
Kai Baukus,
Ben Lukoschus und
Karsten Stahl
sind die Helden dieser Geschichte.
Dieses Werk ist folgendermaßen gegliedert: Wir beginnen mit einer
Liste der Vortragenden und der Zuhörer. Zur besseren Lesbarkeit
wurden diese in einem externen Anhang untergebracht.
Eine extensive Beschreibung aller interessanten Ereignisse gibt in
chronologischer Reihenfolge in Hauptteil. Wir schließen mit einigen
Fragen an den interessierten Leser.
Liste der Vortragenden
Liste der Teilnehmer
[Diese Listen sind nur in englischer Sprache verfügbar.]
Riskiert einen Blick auf die Fotos, die Clara María Segura Díaz gemacht hat!
Technischer Hinweis. Da ich mit einem tragbaren MiniDisc-Rekorder ausgestattet war, konnte ich Unmengen verschiedener Töne während des Aufenthalts in Finnland sammeln. Wenn du also irgendwo das Mikrofon-Symbol
siehst und dein Browser
WAV-Tondateien (16 bit, mono, 11.025 Hz) abspielen kann, einfach
klicken, zuhören und genießen.
In Helsinki mußten wir mit dem Zug weiter nach Turku, aber wir wußten nicht, daß der Bahnhof etwa 20 Kilometer entfernt war. Also fuhren wir mit einem Bus der Finnair dorthin, und wir kamen gerade noch rechtzeitig an, zwei Minuten bevor unser Zug abfuhr.
Das Einchecken im Hotel Centro war schnell erledigt. Karsten und Ben teilten sich ein Zimmer, und Kai hatte zwei Wochen Zeit, um sich an Holger aus Münster zu gewöhnen.
Den Abend rundeten wir ab mit einem Besuch bei McDonald's, wo wir ziemlich beeindruckt waren über die Länge finnischer Wörter für so einfache Dinge wie ``Pommes'' (ranskalaiset perunat).
schlürften einfach ein paar Tassen Kaffee, Tee
oder Kakao.Nach dem Frühstück begaben wir uns auf einen 20-Minuten-Fußmarsch zum Mauno Koivisto Center im Turku Technology Center. Eine ausgeklügelte ``Ampel-Timing-Strategie'' befähigte uns, soviel Zeit wie möglich am Frühstückstisch und so wenig Zeit wie möglich auf den Straßen von Turku zu verbringen.
Ausgestattet mit vielen Papieren, Zeitplänen und wunderschönen, qualitativ hochwertigen Namensschildern, genossen wir eine nette Einführung in Finnland, Turku und seine beiden Universitäten, Universität Turku und Åbo Akademi. Danach sprach Orna Grumberg über Computer-aided verification of hardware and software.
Die erste Kaffeepause entpuppte sich als Kaffee/Tee/Kuchenpause, aber die Kuchen stellten sich als Leberwurstpasteten heraus. Der nächste Vortrag war über Refinement and verification techniques used in security von Martín Abadi, der über Kryptographie und Protokolle sprach, und in einer praktischen Demonstration zeigte er, daß seine Folien wasserfest sind.
Mittagessen gab es im Restaurant Amica nur ein paar Schritte den Flur entlang. Der interessanteste Teil der Mahlzeit war ein seltsames Getränk, das ``home beer'' genannt wurde, eine Art teilvergorenes Bier mit einem Geschmack irgendwo zwischen Sekt und Cola oder etwas völlig anderem. Wir wagten es auch nicht, dieses Zeug ``Flüssigkeit'' zu nennen, daher wurde dafür der Begriff ``Substanz'' eingeführt und benutzt.
Nach dem Essen sprach Ralph-Johan R. Back über Zustände, Agenten und Verträge in seinem Vortag Refinement calculus overview. Der Verweis auf sein neues Buch wurde zum ``running gag'' für die nächsten zwei Wochen, und immer, wenn jemand einen Fehler im Vortrag entdeckte, hieß es ``im Buch ist es okay''.
Am Abend besuchten wir die Museen Aboa Vetus & Ars Nova. Das Aboa Vetus (lateinisch für ``altes Turku'') zeigt mittelalterliche Straßen, Häuser und Keller aus über 700 Jahren der Geschichte Turkus. Interessante Kunstwerke des 20. Jahrhunderts sind im Ars Nova (``neue Kunst'') zu sehen. Wir beschlossen den Besuch mit einem Büffet und Getränken im Café Niki im Museum.
Nach einem weiteren Bier (beziehungsweise einer weiteren Cola) in ``Pappa Joe's Self-Service Banana Bar'' auf einem Boot im Fluß Aurajoki gingen wir zurück ins Hotel und spielten Karten, bis wir müde genug waren zum Zubettgehen.
Die heutigen Vorlesungen waren Orna Grumbergs zweiter Teil CTL model checking, Pamela Zaves Vortag über Specification and verification of telecommunication lines; Reino Kurki-Suonio präsentierte eine Incremental specification in a TLA-based approach to object systems und Ralph-Johan R. Back setzte seinen gestrigen Vortrag fort. Einige Zitate zeigen die Glanzpunkte dieser Vorträge:
Am Abend ging eine ziemlich große Gruppe in die Pizzeria ``Dennis''. Die Pizzen waren sehr gut, aber ich Trottel bestellte Lasagne, und die war überhaupt nicht gut. Ich weiß nicht, ob das Bier gut schmeckte, aber Koen benutzte diese Formulierung, als er die Rechnung bezahlte:: ``Ich hatte Ravioli und ein bieriges Ding.''
Am Nachmittag machten fuhren wir auf einem Boot namens
``Watercat'' (nicht ``Watergate'') auf die Insel Seili.
Während der Überfahrt hatten wir einen unglaublichen Ausblick auf tausende
kleine verstreut liegende Inseln, was typisch für viele skandinavische Küsten
ist. Und es gab einen Angriff von Flugameisen, etwas, was man wirklich nicht
erwartet, wenn man auf See ist.
In der Vergangenheit wurde Seili zunächst als Standort für ein Leprakrankenhaus, dann für eine Irrenanstalt benutzt, und heute befindet sich dort das Archipelago Research Institute der Universität. (Mehr Details gibt es hier.) Ralph-Johan R. Back läutete eine große Glocke neben einer hübschen Holzkirche, und regte damit unseren Fremdenführer auf, der uns erzählte, daß die Glocke nur als Feueralarm benutzt wird.
Das seltsamste an Turku ist der Schornstein des städtischen Elektrizitätswerks. Dort sind große, rote Neon-Ziffern angebracht, und von oben nach unten ist zu lesen: 1 1 2 3 5 8 13 21 34 55, was der Anfang der Fibonacci-Folge ist.
Und falls du jemals Martín Abadi persönlich kennenlernst, frag' ihn nach dem ``Breitmaulfroschwitz''.
Nach dem Essen begann Eric C.R. Hehner mit A practical theory of programming. Da Martin Büchi (der offizielle Summer-School-Fotograf) ziemlich lange versuchte, eine gute Position für ein Foto von ihm zu finden, sagte Eric: ``Kannst du dich beeilen und `klick' machen?''
Die letzte Vorlesung des Tages war Orna Grumbergs letzter Vortrag, den sie mit einer Übersicht über Model Checking und Beweiswerkzeuge beendete.
Am Abend gab es den ``Abend der Künste'', und neben anderen Dingen hörten wir uns einige Bands an, die verschiedeme Musikstile präsentierten:
elektronisch (ein Typ mit einem Computer, ein Mädchen singt)
Popmusik (das Lied heißt ``This is how I am'')
Jazz
Später gingen wir noch in eine Kneipe (``Erik Public House'') und eine Disco (``Puuteri'').
Pamela Zave und Eric C.R. Hehner setzten ihre Vorträge fort. Letzterer erwähnte das Data Refinement Book von Willem-Paul de Roever und Kai Engelhardt in seinem Vortrag (in Wirklichkeit wußte Eric den Namen des zweiten Autors nicht und sagte ``ein anderer Typ''). Warum erwähne ich dieses Buch? Nun, es wurde an unserer Universität in Kiel geschrieben, also los, kauft es! :-)
Um 15:30 Uhr gab es dann ``Questions I'', wo die Teilnehmer die Möglichkeit
hatten, Fragen über die Vorträge der ersten Woche zu stellen.
Da am Anfang niemand wagte etwas zu fragen, begann einer der Vortragenden mit
einer ziemlich langen Frage über offene und geschlossene Systeme:
[Dieser Teil ist nicht übersetzt, da ohnehin fast nur Fremdwörter
darin vorkommen.]
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.''
Nach dieser Diskussion gab es einige Fragen vom Publikum, wie z.B. diese über zwei obskure Beweistricks von Eric
C.R. Hehner:
Koen Claessen: ``Du hast
also zwei dubiose Dinge gezeigt, ...''
Eric
C.R. Hehner: ``Ja.''
Koen Claessen: ``... und du
willst nicht genauer erklären, warum diese dubiosen Dinge korrekt
sind?''
Eric
C.R. Hehner (nach einer langen Pause): ``Nein.''
Ein weiteres wichtiges Thema waren die ``Engel & Dämonen'', die von Ralph-Johan R. Back eingeführt wurden:
Reino Kurki-Suonio: ``Aus deinen
Folien weiß ich, daß User weiblich sind. Aber ich habe nie betrachtet, ob das
auch für Engel & Dämonen zutrifft.''
Ralph-Johan R. Back:``Diese Frage
werde ich nicht beantworten. Ich habe zwar eine Meinung, aber die sage ich
nicht.''
Der heutige soziale Abend war ein Besuch in der Villa Y-Hovi in Ruissalo, wo wir zu abend aßen, und dann gingen wir in die berühmte finnische Sauna. Der Temperaturunterschied zwischen der Sauna (90 °C) und der Ostsee (17 °C) war sehr erfrischend, und alle hatten sehr viel Spaß.
Michel Sintzoff zu Eric C.R. Hehner: ``Du siehst aus wie ein Hummer.''
Um 23 Uhr ging es zurück ins Hotel, und sofort verließen wir es wieder in Richtung ``Puuteri'', wo wir blieben, bis etwa um 4 Uhr der Laden geschlossen wurde. Auf dem Rückweg trafen wir eine völlig betrunkene Frau namens Mira, die mitten auf der Straße saß. Als sie erkannte, das einige von uns aus Deutschland kamen, erzählte sie uns mindestens fünf Mal, daß sie mit ihren Eltern in Deutschland gewesen ist, als sie ein kleines Mädchen war. Und sie war auch in einer Sauna dort. Wir ließen sie etwa zwanzig Minuten lang erzählen. Dann gingen wir weg.
Das Abendessen verspeisten wir in einem Restaurant namens ``Herman'', das ein
bißchen exklusiv war; selbst der nervtötende
Klavierspieler fehlte nicht.
Regen. Wir hatten die Ehre, unseren Frühstückstisch mit Martín
Abadi zu teilen, der Finnland an diesem Tag verließ.
Am Nachmittag regnete es immer noch, also schauten wir uns den Formel 1 Grand
Prix in Ungarn im finnischen Fernsehen an. Während Mika Häkkinen Probleme
mit seinem
McLaren Mercedes hatte, lief der Ferrari seines Rivalen Michael Schumacher
gut, und
``Schumi'' konnte das Rennen gewinnen.
Abendessen gab es im Restaurant ``Ribs''. Auf dem Weg zurück ins Hotel
zeichneten wir ein weiteres finnisches Geräusch auf, das nervige Piepen der Ampeln.
Am Nachmittag folgen wir Ralph-Johan R. Backs Ausführungen und hörten den Vortrag von Amir Pnueli über Verification of reactive systems. Er erzählte uns die wahre Geschichte über Leslie Lamports Abkürzung ``TLA''. ``TLA'' steht für ``three letter acronym'' [``drei-Buchstaben-Abkürzung''], was uns zeigt, das das wichtigste bei der Einführung einer Neuheit ein Name ist, den man gut mit drei Buchstaben abkürzen kann.
Am Nachmittag warfen wir einen Blick auf das Museum Bonk Inc. in Uusikaupunki. Abendessen gab es im Restaurant Kala-Trappi in Naantali. Abschließend machten wir noch eine Kneipentour durch ``Old Pharmacy'', ``Erik'', ``Café Noir'' und ``57''.
Nachmittags besuchten wir das Schloß Turku und lernten viel über die Geschichte
von Turku und das Leben im Mittelalter; nun wissen wir auch, warum
Wendeltreppen im Uhrzeigersinn gebaut wurden. Abendessen gab es im
Burgrestaurant Juhana Herttuan Kellari, wo wir ein excellentes Mahl genossen
und eine Rede von Amir Pnueli, und
wir lauschten mittelalterlicher Musik.
Am Abend fügten wir ``Dynamo'', ``Amarillo'' und ``Opera'' der Menge uns bekannter Kneipen und Discos hinzu.
Abends traf sich eine große Gruppe zu einem letzten Drink in der ``Old School'', und etwas später gingen wir noch ins ``Amarillo''. Da wir am nächsten Tag recht früh aufstehen mußten, blieben wir nicht allzu lang.
Geräusch auf dem Pflaster
des Fußweges. Im Zug nach Helsinki waren auch zwei Niederländer (Victor Bos und Martijn Oostdijk), und wir trafen
uns später nocheinmal im Bus zum Flughafen Helsinki.
In Helsinki hatten wir einige Stunden Zeit, bevor unser Flugzeug nach Hamburg
startete. Wir latschten ein bißchen herum und hörten uns ein wenig traditionelle finnische Musik an. Mittag hatten wir im Restaurant
Planet Hollywood, wo wir einige
anständige aber ein wenig teure Hamburger verzehrten. Das definitive audiophile
Glanzlicht dieses Reiseberichts ist natürlich die Klospülung in der Herrentoilette im Planet
Hollywood Helsinki.
Im Flughafen trafen wir wieder ein paar bekannte Gesichter, bevor wir dann unseren Flug IB 6943 nach Hamburg antraten. Übrigens: Wenn man die Lautsprecherdurchsagen auf Flughäfen wirklich verstehen möchte, sollte man auf die Toilette gehen, weil dort die Akustik wesentlich besser ist.
Im Hamburg hatten wir nur 13 Minuten, um unser Gepäck zu holen, bevor der Bus nach Kiel abfuhr. Irgendwie schafften wir das.
