FMOC 2002 – Leiden, 4 – 8 november 2002

In het kader van mijn sabatical (halftijds van juni tot en met november) bezoek ik ook FMOC (workshop on Formal Methods for Objects and Components) dat plaatsvindt aan de Leidse Universiteit.

Maandag 4 november 2002.

Omdat de workshop al ’s morgens vroeg begint, reis ik de avond ervoor al af. Ik vertrek rond half zeven ’s avonds van huis en reis per auto in ruim twee en een half uur naar Leiden. Onderweg is het rond Schiphol behoorlijk mistig maar verder verloopt de reis voorspoedig. Het hotel (het witte huis) is snel gevonden en de kamer is ruim en geschikt voor wel drie personen. Parkeren rond het hotel lijkt wat problematisch, maar dat is omdat er verschillende vergaderingen in het hotel worden gehouden en alle (gratis!) plaatsen zo’n beetje bezet zijn.

Ik bel naar huis dat ik er ben, kijk nog wat tv en ga op tijd naar bed.

Dinsdag 5 november.

Na een redelijke nacht slapen zit ik rond acht uur ’s morgens aan het ontbijt. Dat is wat karig, er is niet veel keuze, maar de broodjes, jus, thee en cornflakes smaken toch goed. De ontbijtruimte is deel van het restaurant en is ingericht met allerlei oude spullen, zoals wasteilen, lieslaarzen, visnetten en tennisrackets.

Dan per auto naar het Gorlaeus-lab, een modern rond gebouw op het science park van de universiteit van Leiden. Bij de registratie ontvang ik een schrijfmap en een tas met FMCO-opschrift. Ook een paraplu behoort tot de set.

Marcello Bonsangue van de UL opent het symposium en meldt o.a.\ dat dit de eerste FMCO is, maar zeker niet de laatste.

Bertrand Meijer (ETH Z”urich) opent de rij sprekers. Hij spreekt over trusted components. In de intro maakt hij o.a.\ reclame voor een nieuw tijdschrift: Journal on object technology, (zie www.jot.fm). Bertrand merkt op dat de kwaliteit van software een belangrijk issue is, maar niemand het eigenlijk veel lijkt te deren dat de kwaliteit in het algemeen niet gehaald wordt (behalve als het om veiligheid gaat). Er zijn twee mogelijke vormen van aanpak: a priori (build it right) en a posteriori (validate and fix it). Belangrijk in dit verband is het realiseren van goede componenten. Een quote: “component design should be formula-1 racing of software engineering.” M.b.t. de software-as-it-is volgt Meijer de low road, resulterend in een component certification center aan de ETH en m.b.t. software as it should be volgt hij de high road, met o.a.\ een general framework for proving classes. Hij is bezig een component quality model te ontwikkelen waarin een groot aantal criteria zijn verzameld, nl.\ social (some reuse attested/producer reputation/published evaluation), functional (examples/usage docs/preconditioned/some postconditions/full postconditions/observable invariants), performance (o.a. platform specs/response time/security), design (precise dependency doc/consistent api rules/strict design rules/proofs of pre- c.q. postconditions and invariants) en extension (portable across platforms/uitbreidbaar/user action pluggability).

Bertrand noemt o.a. een systeem in gebruik bij de Parijse metro als voorbeeld van proof technology and formal methods. Als gevaar noemt hij dat slechts specifieke properties van componenten kunnen worden bewezen: niet de hele component is daarmee “correct.” Wel vindt hij dat de extra inspanning van het gebruik van formele methoden loont als de componenten worden hergebruikt.

Nog een paar quotes: “the biggest hope and chalenge for software industry is at the confluence of formal methods and reuse.” en ”now it is time to do it.”

In de koffiepauze kom ik Hendrik Wietse de Haan (aio bij Wim H. en Gerard R.) tegen. Toch nog een andere Groninger aanwezig op dit symposium.

Na de koffie spreekt Farhad Arbab (CWI) over abstract behaviour types (ABT’s). Hij start met een intro over ADT’s en het feit dat deze de fundamenten vormen voor OO-programming (ADT-operaties zijn de class methoden). Dan introduceert hij een ABT, waarbij o.a. asynchrone communicatie uitgedrukt kan worden. Een ordening van events, een zg. infinite stream, vormt hiervan de basis. Zo ontstaat een zg. timed datastream, een input/output achtige notatie. Middels een formule wordt bijvoorbeeld uitgedrukt dat wat erin gaat er ook weer uit moet en dat dat op hetzelfde moment moet gebeuren.

Farhad claimt dat ABT’s krachtiger zijn dan reguliere expressies en een waarschijnlijk ideale basis vormen voor components en hun compositie. Ik ben hiervan nog niet helemaal overtuigd en, gezien de vragen, het publiek na afloop ook niet.

Martin Wirsing (University of Munich) spreekt dan over “making components move: a seperation of concerns approach” waarbij het concept van global computing wordt geformaliseerd (de computation is verdeeld over een netwerk en is zeer dynamisch). Zowel code, agents als components zijn verhuisbaar. Martin legt de algebra Basic Sail uit, waarmee dit idee formeel vormgegeven kan worden. Het verhaal is erg theoretisch en in mijn opinie nog ver weg van mogelijke toepassingen.

Dan is het lunchtijd. Broodjes, beleg en een zalmsalade vormen de belangrijkste ingredïenten.

Na de lunch houdt David Harel (Weizmann institute of Science, Israel) een zeer boeiende lezing over zijn play-engine. David start met allerlei vooroordelen en verkeerd gebruik van formele en visuele talen (noemt UML als voorbeeld daarvan). Dan legt hij de huidige structuur van ontwikkeling van systemen uit:

waarbij de use cases worden gebruikt als informele vorm van de requirements. De structure wordt weergegeven middels object model diagrammen en de behavior middels state charts. Harel geeft een voorbeeld uit de biologie om één en ander te verduidelijken. Als belangrijkste visuele formalisatie voor de requirements wordt de message sequence chart (MSC) gebruikt (het sequence diagram uit UML). Het gedrag kan echter op twee manieren worden bekeken: (1) scenario based (geef, middels “verhalen”, het interobject gedrag weer) en (2) behavior based (geef het i/o gedrag per object/component weer). Er is consistentie als het scenario based gedrag klopt met het gedrag per object/component.

Requirements moeten echter rijker zijn en meer informatie bevatten. Daarom is de LSC (life sequence chart) bedacht. Een LSC bestaat uit een prechart (het if-stuk, de oude MSC) en een mainchart (het then-stuk, waarin allerlei extra condities zijn op te nemen).

Vervolgens komt Harel met een telefoondemo waarmee hij illustreert dat het voldoende is zijn play-engine te voeden met scenario’s (door deze simpelweg uit te voeren) waarbij de engine er de juiste LSC’s bijmaakt. Uiteindelijk ontstaat in feite een tussenvorm tussen use cases en requirements in de vorm van een zg. played behavior. De gespeelde bedrag dient als input voor de requirements (play in) waarna de requirements middels play out, en buiten het systeemmodel om, in staat is de applicatie te vormen. Er is dus geen systeemmodel meer nodig en ook geen codegeneratie. De play-out (uitvoeren van het programma nadat slechts scenario’s zijn aangeleerd) is mogelijk doordat daarbij zeer strikt de aangeleerde regels worden nageleefd: “universal charts drive the execution.” Harel werkt nog aan een manier om een soort backtracking te realiseren in de play-out. Nu wordt daarin simpelweg de eerste de beste goede stap gedaan.

Vraag van mij (en van het publiek) is hoe complex een en ander wordt bij wat grotere applicaties. Uiteindelijk moeten steeds alle regels worden gecontroleerd. Binnenkort komt hierover een boek uit met als werktitel “let’s play.” De huidige software is voor wetenschappelijke doeleinden vrij beschikbaar.

Na de thee spreekt Joseph Sifakis (Verimag, Frankrijk; ik ken hem nog van WODES96 in Edinburgh) over composition for component based design. Joseph begint met een oud probleem, nl. het syntesis problem: gegeven een component C en een property P, vindt een nieuwe component C’ en een compositie, zodat de compositie van C en C’ leidt tot de gewenste property P. Dit lijkt veel op het aloude probleem dat ik in mijn thesis heb opgelost, maar nu veel algemener gesteld. Verderop in zijn verhaal verdeelt hij events in twee deelverzamelingen: complete en incomplete actions (complete betekent: hier kunnen we stoppen, incomplete betekent dat we nog niet klaar zijn na deze actie). Dat lijkt weer erg op mijn verdeling in exogene en endogene events.

Het verhaal past zo in een WODES-conferentie. Uiteindelijk gebruikt Joseph prioriteiten om extra restricties op te leggen (de ene actie heeft hogere prioriteit boven de andere) en lost zo o.a. wat deadlockproblemen en mutual exclusion op.

Het is allemaal erg theoretisch en het verhaal bevat slechts simpele voorbeelden. Toch claimt Joseph dat hij de theorie al toepast in een java-dialect: “real-time” java.

De laatste spreker van de middag is Amir Pnueli (Weizmann institute of science, Israel). Amir is blijkbaar erg ijdel want hij heeft een bekende lok haar van links naar rechts over zijn verder kale hoofd! Zijn verhaal over compositional approaches to temporal verification bevat erg veel temporal logic en kan me niet erg boeien.

Tegen vijf uur ga ik Leiden nog even in en eet een hapje bij V&D. Deze gaat, in tegenstelling tot die in Groningen, gewoon om zes uur dicht en in ben de laatste die in door de keuken nog geholpen wordt. Leiden is een prachtige oude stad met veel bezienswaardigheden. ’s Avonds tik ik alvast weer een stuk van dit reisverslag uit op mijn meegenomen laptop die overdag bij de receptie in bewaring is gegeven.

Woensdag 6 november.

Na een goede nacht slapen en eenzelfde ontbijt als gisteren vangt om negen uur de eerste lezing van deze dag aan. De oorspronkelijke spreker Werner Damm (Oldenburg) laat zich door een collega (Ernst-Rudediger Olderog) vervangen, die echter weinig van de inhoud van het praatje weet. De spreker heeft het over “a formal look at UML”, waarbij o.a. aan de hand van een treinvoorbeeld eerst wat diagrammen worden gegeven (class diagram en state charts). Vervolgens wordt van o.a.\ deze diagrammen de semantiek beschreven middels formele definities. Daarna wordt een formeel transitiesysteem beschreven (om de huidige toestand van het hele systeem bij te houden). De hele toestand (incl. in welke toestand in de state chart het systeem zich bevindt) plus alle attribuutwaarden wordt in een soort vector opgeslagen.

Dan blijkt dat je op een formele manier door de toestand van het systeem kunt lopen en bijvoorbeeld kunt aangeven wanneer welke events geaccepteerd kunnen worden. Ook de LSC’s van Harel komen in het praatje weer terug. Zo kan ook verificatie plaatsvinden.

In het vragenrondje volgt een flinke discussie waarbij blijkt dat het publiek nog lang niet overtuigd is van het feit dat de gepresenteerde techniek formele verificatie mogelijk zou kunnen maken. Bovendien vinden een aantal vragenstellers UML maar rotzooi, dus waarom die rotzooi dan ook nog verder formaliseren. De discussie bewijst m.i. dat hier de theoretici voorbij gaan aan praktisch nut.

In de koffiepauze heb ik een gesprek met C. Pronk van de TUD waarbij o.a. de solicitatie van Jan Bosch in Delft nog weer aan bod komt (nu Jan het aanbod op een laat moment heeft afgeslagen zit de SE-groep in Delft nog steeds zonder hoogleraar). Zo’n 12 jaar terug blijkt ook Gerard Renardel daar een aanbod op een heel laat moment te hebben afgeslagen. Pronk klaagt over het slechte management in Delft (en noemt in dit verband o.a. de vroegere SE-hoogleraar van Katwijk, die nu decaan is.

Na de pauze spreekt Rustan Leino (van Microsoft) over Extended Static Checking for Java. De combinatie Microsoft-Java laat zich verklaren doordat Rustan dit werk heeft gedaan bij compaq.

Rustan geeft een schema waaruit blijkt dat typechecking met weinig effort gedaan kan worden maar ook een lage coverage heeft. Program verification kan een hoge coverage hebben, maar kost in het algemeen ook veel effort. Er blijkt een tussenweg te zijn middels light weight formal methods, waarbij extended static checking een vorm is.

Er volgt een prima demo waaruit blijkt dat ESC/Java in staat is de java-code te verificeren en waarschuwingen geeft als dingen mogelijk niet goed zijn. Dit kan doordat in de Java code annotaties kunnen worden opgenomen. ESC/Java bevat een automic theorem prover. Nadelen van deze aanpak zijn: niet alles kan echter worden gedetecteerd, soms wordt onnodig gewaarschuwd en er is annotatie-overhead en de vertaling duurt langer.

Gerelateerde onderwerpen zijn de java modelling language (Leavens), LOOP (Jacobs) en JML+Junit (Cheon en Leavens). Als vervolgonderzoek noemt Rustan checking components in plaats van classes (dan zal er meer inference zijn en minder specifications).

ESC/Java kan worden gedownload via research.compaq.com/SRC/esc (ook de sources zijn beschikbaar).

Een aardig verhaal waarbij ik zeker naar de weblocatie zal kijken (en het onderwerp kort kan noemen in mijn SAO-college). Tijdens het vragenrondje blijkt nog wel dat ESC/Java nog niet zo krachtig is: de meeste postcondities zijn true met als gevolg dat bijvoorbeeld van een sort-routine niet bewezen kan worden dat deze een sortering uitvoert.

Dan spreekt John Hatcliff (Kansas) over integrated development, analysis, verification environment for component based systems. Als voorbeeld wordt Boeing genoemd waar een gevechtsvliegtuig wordt ontwikkeld waar vele systemen (componenten) op verschillende momenten dienen samen te werken. Hatcliff beschrijft een integrated environment for building and modelling Corba Component systems, genaamd Cadena.

Tijdens de lunch heb ik een gesprek met de bij Philips werkende Pool Leszek Holenderski (wat “uit Holland” betekent). Leszek heeft eerst bij de TUE gewerkt en nu, sinds twee jaar, bij Philips Natlab. Hij vindt zijn huidige baan een paradijs omdat hij geen onderwijs meer hoeft te geven (en dus geen Nederlands hoeft te leren) en, vanwege het registreersysteem, nu een werkdag heeft van precies acht uur.

Na de lunch spreken Emil Sekerinski (McMaster Uni, Ontario) en Kaisa Sere (TUCS) over resp. stepwize refinement of concurrent oo-programs en component based design using action systems. In beide gevallen komen er flink veel predicate transformers en dergelijk op het scherm. Beide praatjes kunnen me, zeker na de lunch, absoluut niet boeien.

Even na drieën hebben we een moment voor ons zelf voordat om vijf uur het social event begint. Dat geeft me de gelegenheid (net voor er een flinke bui losbarst) om nog een ansichtkaart voor Lenie te kopen en op de bus te doen (omdat ik een briefje op het kussen vergeten ben!)) en nog even terug naar het hotel kan om het verslag van vandaag in te tikken.

Even voor vijf uur ga ik op weg naar het museum voor volkskunde. Ik parkeer mijn auto in de buurt op een parkeerplaats waar het na zes uur gratis parkeren is. Problemen met het parkeren heb ik tot op heden in Leiden overigens ook nog niet gehad. Voor de wandeling van zo’n tien minuten van de auto naar het museum komt de verstrekte paraplu zeer goed van pas. Het regent nu best. Eenmaal in het museum schijn ik zo’n beetje de eerste de zijn. Pas een kwartier na vijf uur komen er plotseling zo’n dertig man binnen. Ze hebben allemaal bij de ingangspoort in de regen staan wachten. Het museum is gevestigd in het voormalige academische ziekenhuis (het eerste academische ziekenhuis in Nederland) en pas onlangs van binnen helemaal verbouwd. Het museum herbergt een imposante collectie van zaken uit alle delen van de wereld. We krijgen in kleine groepjes een rondleiding door \’e\’en onderdeel van het bedrijf (ik ga voor Afrika) en mogen de rest op eigen gelegenheid bekijken. Verder krijgen we hier de nodige drankjes en aan het eind ook wat warme hapjes aangeboden. Ik spreek o.a.\ met Jos Warmer van het tweemansbedrijf Klasse Objecten. Jos legt uit dat het bedrijf een aantal jaren geleden is opgericht, eerst veel cursussen aan bedrijven heeft verzorgd, en nu ook eigen onderzoek doet, o.a. op het gebied van modellering en ocl.

Jos weet de weg en samen lopen we voor de groep uit even naar zeven uur naar het restaurant “het prentenkabinet”. Ik zit uiteindelijk o.a. samen met Jos, Perdita Stevens (Edinburgh University; haar Engels is echt Engels!), Bernard Rumpe (Munchen), C. Pronk (TUD), Manfred Broy (Munchen) en nog wat andere Duitsers aan een tafel. We hebben het vanzelfsprekend over UML en formele zaken (de sprekers die tijdens FMCO UML omzetten naar iets formeels hebben blijkbaar de specificatie van UML zelf nog niet gezien, want vertalen alleen de diagrammen), over email (en hoe van de lange lijsten nog te beantwoorden emails af te komen), over het BaMa-systeem en de oude systemen in Engeland en Duitsland en nog veel meer.

Het diner zelf is prima. Zalm vooraf, een kippeboutje als tweede voorgerecht, biefstuk als hoofdgerecht en crême brullé (met een hoopje ijs) als toetje. Koffie en eventueel een likeurtje complementeren het geheel. Voor het dessert spreken Marcello Bonsangue en Frank de Boer de eters toe. Marcello legt uit dat we ons eigenlijk bevinden in een ruimte waar vroeger onder toeziend oog van studenten op de ballustrade mensen werden ontleed en dat de ruimte later als bibliotheek is gebruikt. Frank maakt er ongewild een soort dank-je-wel speech van en bedankt o.a.\ de sponsors en de deelnemers. De tweespraak krijgt, mede door de genuttigde wijn, een vrolijke toon.

Rond tien uur is het diner ten einde en ga ik, het regent nog steeds, terug naar mijn hotel.

Donderdag 7 november.

Alle gezichten bij het ontbijt blijken van het congres te zijn. Voor de eerste lezing kom ik Jan van Schuppen tegen, die eigenlijk het hele congres wel had willen meemaken, maar blijkbaar allerlei andere verplichtingen heeft (waaronder het bezoek van de loodgieter bij hem thuis morgen). We spreken nog even kort over mijn postdoc, Ahmed Al-Falou, die vooral bij Jan zijn werkzaamheden heeft verricht. Ahmed heeft nu een baan bij een bank in Duitsland.

De eerste lezing is van Clemens Szyperski (Microsoft) met als titel “components meet web services.” Clemens heeft het over componenten bij softwareontwikkeling als “losse” onderdelen die een belangrijke rol spelen in dynamic upgrades, extensions en bij integratie. Hij noemt het component maturity model (CMM). Een software component is “a unit of deployment” ofwel “a collection of modules and resources” (waarbij de modules de statische code en de resources de statische data voorstellen, resp. de verzameling classes en de immutable objects).

Uiteindelijk beweert Clements dat een component meer informatie dient te bevatten dan nu gebruikelijk is. Zo zou in de component bijvoorbeeld bekend moeten zijn wat de build environment is, referenties naar artifacts, alle gebruikte tools, de sources e.d. Dan kan pas goed aan versiebeheer worden gedaan (zodat bijvoorbeeld kan worden nagegaan met welke versie van welke vertaler de code gemaakt is).

Er is overigens een versieprobleem, want wat gebeurt er als component B afhangt van versie 1 van component A en C van versie 2 van A en daarna D weer afhangt van B en C? Welke versie van A wordt dan uiteindelijk genomen?

Daarom wordt gepleit voor het meenemen van de versie-informatie in de naam van de component en dient ook bij afhankelijke componenten te worden aangegeven van welke versie van welke andere componenten ze afhankelijk zijn.

Dan spreekt Clemens over services als zijnde een instantiated configured system plus providing organization (ofwel alle static dependencies zijn “all the way down” bepaald). Nu kan gesproken worden van een technisch contract (specificatie van een component, is exact) en een service contract (waarbij niet alles meer exact kan worden bepaald).

Als conclusie stelt hij uiteindelijk dat als er geen formele dingen aanwezig zijn versiecontrole nodig is en alleen componenten van precies de goede versie echt bij elkaar passen. Zijn er formele specificaties voorhanden dan kan dit worden verruimd door te stellen dat componenten gelijk zijn zolang hun specificaties maar gelijk zijn en passen verschillende versies beter bij elkaar.

Verweving van specificatie en implementatie wordt middels een voorbeeld in AsmL (abstract state machine language) uitgelegd. Zie ook research.microsoft.com/fse/ (voor een gratis betaversie).

Na de koffiepauze spreekt Oscar Nierstrasz (Bern) over “towards a practical composition language?” Hij spreekt over Piccola, een kleine compositietaal die in staat is om componenten te koppelen.

In Piccola worden Forms gebruikt om de structuur (sequence of bindings) aan te geven, Agents voor het gedrag (executing scripts) en Channels voor de toestand. Een script koppelt componenten aaneen door services aan te roepen.

In de verte lijkt deze aanpak wel wat op onze feature based composition. Piccola is overigens nog lang niet volledig. De spreker noemt nog allerlei missende zaken.

David Garlan (Carnegie Mellon) heeft het daarna over self-healing systems. Hij geeft een aardige schets van de geschiedenis en de nabije toekomst van de computers en noemt achtereenvolgens het tijdperk van de mainframes (1 computer per 100000 mensen), tijdperk van de desktops (1 op 100), van de netwerken (1 op 1; de huidige situatie met als belangrijkste issues het vinden van informatie, junk (in mail e.d.) en veiligheid) en voor de nabije toekomst het tijdperk van ubiguetous computing (100 computers per persoon). Belangrijke consequentie in dit nieuwe tijdperk zijn dan dat alle systemen met elkaar verbonden zijn en eigenlijk altijd (dienen te) draaien, uit componenten van velerlei producenten zijn opgebouwd, in wisselende omgevingen met wisselende resources werken en gebruikt worden door mobiele gebruikers. Een paar dagen stopzetten om een foutje op te lossen gaat dan niet meer, off-line repair is niet langer een optie.

Het systeem dient nu automatisch en optimaal adaptief te handelen in geval van veranderde behoeften van de gebruiker, variabiliteit van resources, fouten en mobiliteit. Ofwel systemen dienen self-healing te worden. Noodzakelijk hiervoor zijn nieuwe eisen, zoals refection (kunnen zien waar het systeem zich bevindt, hoe het zich gedraagt e.d.), self-adaptation, context awareness, en task driven zijn. In feite gaan we van een openloop systeem naar een closedloop systeem waarbij het systeem middels een controller wordt bijgeregeld.

De “regelaar” bekijkt het systeem, detecteert bijvoorbeeld fouten en gaat dan zelf, met de in de regelaar aanwezige specificatie op zoek naar aanpassingen, probeert dit eerst uit op de specificatie en als het voldoet wordt de wijziging in het systeem ingevoerd.

Hieruit volgt dat formele specificaties belangrijk worden als run-time artifact en formele methoden nodig zijn voor de specificatie en de analyse. Refinement krijgt een andere betekenis, niet meer van abstract naar concreet, maar wordt een run-time relationship.

Op het web, zie www.cs.cmu.edu/~able of www.cs.cmu.edu/~aura is meer hierover te vinden.

Na afloop wordt herhaaldelijk gevraagd in hoeverre control theory hier een rol kan spelen, bijvoorbeeld m.b.t. stabiliteit.

Tijdens de lunch spreek ik met Frank de Boer. Het symposium is een succes en hij is verbaasd dat veel invited speakers meerdere dagen blijven en ook bij veel praatjes aanwezig zijn.

Na de lunch spreekt Manfred Broy (Munchen) over specification, composition, and decomposition of software components. Hij heeft het over systemen geconstrueerd middels componenten en verbonden middels channels. Die channels worden gemodelleerd m.b.t. timed streams (per discreet tijdsstip kunnen verzamelingen messages worden verstuurd). De streams lijken op traces, maar bevatten per tijdstip een verzameling messages. Een service-interface heeft nu een input- en een outputstream.

Het getoonde model combineert fundamentele technieken (verificatie) met grafische weergave (zichtbaarheid). Implementatie van het geheel gaat middels state machines, waarbij bewezen kan worden dat de SM voldoet aan de gegeven specificaties van het model.

Er is gewerkt aan toolsupport dat ook al door verschillende bedrijven schijnt te worden gebruikt.

Na de theepauze spreekt Ernst Ruediger Olderog (Oldenburg) over specificaties met CSP en Object-Z. CSP wordt gebruikt voor proces-specificatie, data wordt gespecificeerd middels Object-Z, waaruit de mix CSP-OZ is gemaakt. Het proces- en het datagedeelte synchroniseren middels de CSP-synchronisatie. Tijdens de vragen blijkt dat alleen nog maar kleine systemen kunnen worden aangepakt, o.a.\ vanwege de modelchecker.

Dan spreekt Leslie Lamport over “high-level specifications, lessons from industry.” Zijn slides zijn klaarblijkelijk met LaTeX gemaakt, en worden via acrobat getoond. Leslie houdt een vlammend betoog over de specificatietaal TLA+ en de model checker TLC en komt tot de conclusie dat zaken als typering, information hiding, OO, componenten en hierarchie in specificaties niet nodig zijn. High level specificaties moeten simpel zijn: “do not use programming languages for specification, use a high level specification language instead.”

Na afloop is er een lange discussie. Bijna alles wat deze dagen gepresenteerd is, zou volgens Leslie veel te veel van het goede zijn en dat geeft, na enige aarzeling, toch wel wat protesten vanuit de zaal.

Na de tweede theepauze spreekt Ugo Montanari (Pisa) over “composing systems with name mobility.” Hij heeft het over algebra’s, co-algebra’s en tovert voortdurend allerlei, voor mij onbegrijpelijke, formules op het scherm.

’s Avonds eet ik in het hotel. De menukaart op mijn kamer blijkt oud: het daar al uitgezochte menu blijkt op de nieuwe kaart te ontbreken. De ober is boos omdat de oude kaarten allang door nieuwe vervangen hadden moeten worden. De hulp-ober wordt door dezelfde man overigens behoorlijk achter zijn broek gezeten. Het eten smaakt overigens goed.

Vrijdag 8 november.

Eerste spreekster vandaag is Perdita Stevens. Zij heeft het over “playing games with UML tools.” Ze begint met een korte uiteenzetting van de ontwikkeling van software design (lijkt op een eerste college analyse en ontwerp): olden days de watervalmethode, jaren 80 Boehms spiral, begin jaren 90 OO als silver bullet, eind 90 UML als standaard voor rapportage daarnaast UP als standaard ontwikkelproces versus agile methodologien als XP, waarbij beide langzaam naar elkaar toegroeien.

Perdita legt uit dat voor UML nu veel verschillende tools beschikbaar komen, maar dat die tools in het algemeen erg duur zijn. De tools helpen eigenlijk meer met het rapporteren van ontwerpbeslissingen dan met het maken van die beslissingen zelf.

Design is groepswerk en zou kunnen worden beschouwd als het spelen van een spel. Ze legt uit wat bisimulation is (een refuter die probeert een tegenvoorbeeld te bedenken en een verifier die elke stap van de refuter probeert te beantwoorden).

Eenzelfde spel kan ook gespeeld worden met design. Voor zo’n game is nodig de startposities te kennen, de mogelijke moves en de winning conditions. Het maken van de game is de design, het spel spelen de verificatie ervan.

Ze concludeert haar prima voordracht uiteindelijk met de feiten dat UML helpt bij zowel competition als cooperation tussen tools en techniques en dat meer tools nodig zijn in de designfase, waarbij het verder uitwerken van games in dit opzicht zo’n tool zou kunnen zijn.

Na de pauze begint Bernhard Rumpe (Munchen) met zijn verhaal over “interplay and testing and refactoring within UML” en start zijn praatje met reclame voor een nieuw tijdschrift: Software en Systems modeling (zie www.sosym.org).

Bernard begint met wat slides over UML. De relevantie van UML wordt benadrukt (UML is de gemeenschappelijke “taal” dus verstaat men elkaar beter; mensen denken het liefst in plaatjes; is nu standaard, dus betere toolsupport; UML is een goede taal om wetenschappelijke resultaten aan niet wetenschappers uit te leggen; en diagrammen zijn niet pers\’e informeel), maar helaas zijn er mensen die tekst prefereren boven diagrammen (hij noemt Edgar Dijkstra, Bertrand Meijer en Kent Beck). Toolsupport zou deze mensen wellicht kunnen overtuigen. Hij noemt ook wat problemen met UML (geen goede preciese semantiek; te groot; en tussenvorm tussen natuurlijke taal en formele taal en daardoor door geen van deze partijen goed bevonden) en zegt dat door de verdere standaardisatie van UML ook alle huidige flaws worden gestandaardiseerd en doet de suggestie wellicht met een Europese variant te beginnen.

Dan gaat hij verder met een verhaal over software evolution (software steeds aanpassen vanwege veranderende omgeving, requirements, e.d.) en behalve de code dient dan ook het model aangepast te worden. Dit zou kunnen door het oorspronkelijke model te transformeren naar het nieuwe model, waarmee de noodzaak voor transformatietechnieken aangetoond is.

Hij geeft een voorbeeld van zo’n transformatie (op de code!) waarbij eerst bepaald wordt wat anders moet, dan dat nieuwe element wordt toegevoegd en een invariant bedacht die oude datastructuur en nieuwe datastructuur logisch met elkaar verbindt. Dan kan extra code worden toegevoegd op de nieuwe structuur waarbij de invariant moet blijven gelden en tot slot kan code op de oude datastructuur worden verwijderd en tot slot ook de oude datastructuur zelf.

Dan spreekt Paul Klint (CWI) over de toolbus. De toolbus is een programmeerbare connector tussen software mogelijk geschreven in verschillende talen en draaiend op verschillende machines. Toolbus is dus een programmable software bus waarbij op procesalgebra gebaseerde scripts dienen voor de connecties. De scripts zorgen voor de coordinatie, een special data exchange format zorgt voor de data exchange.

Paul geeft een statusreport van Toolbus en noemt drie belangrijke issues waar verder onderzoek naar gedaan dient te worden, namelijk de send-receive paren (in Toolbus opgelost door send en receive wel in paren te laten voorkomen maar tussentijdse acties mogelijk te maken), exception handling en call-by-ref verses call-by-name.

Dan is het lunchtijd.

Jos Warmer van Klasse Objecten spreekt na de lunch over OCL en de rol van OCL in model driven architecture.

Jos begint met de rol van modelling in softwate development en noemt vijf model maturity levels: mml-1: textuele modelling (in natuurlijke taal); mml-2: tekst en diagrammen (waarbij de diagrammen de tekst verduidelijken); mml-3: modellen met tekst; mml-4: preciese modellen (met hooguit wat aanvullende verklarende tekst in een natuurlijke taal); mml-5: models only. OMG noemt mml-4 de model driven architecture, mml-5 is nog toekomstmuziek. UML wordt niet gebruikt in level 1, een beetje in 2 en veel in 3 en 4. level 4 gebruikt daarnaast ocl.

MDA is in feite een transformatie van platform independent model (PIM) naar een platform specifiek model (PSM). De PIM is in UML, de PSM in bijvoorbeeld java, j2EE, SQL, XML, etc. Er kunnen zg.\ bridges worden gemaakt tussen de verschillende PSM’s.

Dan doet Jos het een en ander uit de doeken over OCL en beschrijft vervolgens het MDA-framework. de specificatietaal OCL is een pure expressietaal (zonder side-effects), easy-to-use, precies (formeel en niet ambigu). OCL kan alleen gebruikt worden in combinatie met UML. OCL-gebruik van pre- en postcondities leidt tot Analysis by Contract. OCL is ook een query taal (zoals SQL) en wordt o.a. door het bedrijf Boldsoft gebruikt om userinterfaces te beschrijven.

Het MDA framework beschrijft de transformatie van PIM naar PSM naar code. De transformatiedefinitie beschrijft in feite de transformatie van de ene taal naar de ander. Aangezien een taal van een model in een metataal kan worden uitgedrukt komt het betoog van Jos neer op het feit dat alles in een taal beschreven kan worden. Zo is de metataal voor UML in UML uit te drukken en is, in onderstaand voorbeeld, in een UML-model een Person-class een instantie van een Class-class uit het metamodel.

Een transformatie definitie beeldt elementen van de bron af op elementen van de bestemming, gebaseerd op de respectivelijke modeltalen, ofwel een transformatiedefinitie is geschreven in een transformatiedefinitietaal.

Tot slot heeft Jos het kort over het gebruik van OCL in MDA, nl.\ om modellen precieser te maken, om modellen te beschrijven, om transformaties te beschrijven en geeft een website waar alvast gekeken kan worden naar de submissie van OCL2: www.klasse.nl/ocl/subm-intro.html

Op een vraag uit de zaal wat nu de stand van zaken m.b.t.\ OCL is, antwoordt Jos dat de meeste mensen nog wachten op OCL-tools en dat de alternatieve syntax (o.a.\ door Klasse Objecten gedefinieerd) wellicht toch beter wordt gelezen door mensen uit het bedrijf.

Na de thee spreekt Bart Jacobs (Nijmegen) over wp-reasoning in Java. Middels JML (zie volgend praatje) kan extra specificaties aan Java-code worden toegevoegd. In Nijmegen wordt onderzocht hoe de interactieve verificatie hiervan kan plaatsvinden. Bart gebruikt geen Hoare-triples maar vanwege zaken als exception handling en site effect n-tuples met daarin allerlei extra condities e.d.\ om ook het exception-gedrag e.d.\ te kunnen beschrijven. Voor JavaCard (uitgeklede Java versie voor smartcards) zijn al heel aardige resultaten geboekt. Als belangrijkste issue voor de toekomst noemt hij scalability (bewijzen van correctheid van programma’s moeten sneller kunnen en voor grotere systemen kunnen worden uitgevoerd).

Gary Leavens (IOWA State University) heeft het daarna over JML (zie ook www.jmlspecs.org). JML is een interface specificatie taal voor detailed design en bevat o.a.\ pre- en postcondities en invarianten. Er is support voor zowel runtime checking als statische verificatie (laatste in bijvoorbeeld Nijmegen, zie vorige praatje). Gary roept mensen op die met formele methoden voor Java werken zich bij hem te melden en bij de groep aan te sluiten.

Een JML-spec definieert zowel de interface als het gedrag. De code is correct als het voldoet aan de interface en aan het gewenste gedrag. Gary stipt in zijn betoog nog allerlei problemen aan met JML, zoals notatie, inheritance, side-effects in assertions, toevoegen van eigen types aan de assertions, enz.

Dan is het tegen vijf uur en ik besluit het allerlaatste praatje over te slaan. Ik eet nog snel wat in het brugrestaurant over de A4 en hoop daarna snel thuis te zijn. Dat valt nogal tegen: ik doe zo’n twee uur over het stuk tussen de afslag op de A4 naar de A9 en Almere. Zo’n anderhalf uur later ben ik, ondanks het slechte weer (veel regen), weer thuis en kan ik mij richten op mijn verjaardag, morgen!