We kennen in Nederland een stelsel van basisregistraties. Al ver in de vorige eeuw was daar al sprake van. Het wil echter nog niet zo vlotten. Het paradepaardje van dit stelsel, de basisregistratie personen (BRP), is “slechts” nog in aanbouw, maar er staat inmiddels wel een concept-wet BRP klaar om de bestaande Wet gemeentelijke basisadministratie persoonsgegevens te vervangen.

Waarom duurt dat zo lang? Is het zo moeilijk? Het wetenschappelijke antwoord is: Ja, want de betekenis van gegevens verschilt voortdurend. Een voorbeeld: Het is vandaag de dag nog mogelijk dat de gemeente Amsterdam weet dat u op de Warmoesstraat 53 in Groningen woont, terwijl het CJIB denkt dat u op de Dorpsstraat 13 in Loenen woont. Gewoon, als gevolg van een administratief foutje, dan wel een gebrekkige afstemming, of misschien zelfs fraude. Het idee van de basisregistraties is: één waarheid voor de overheid. Je hoeft geen informaticus te zijn om te snappen waarom dat een goed idee is.

Kennelijk vindt men het ideaal van één waarheid, of tenminste één administratieve werkelijkheid, heel lastig. Er zijn dan ook gewichtige werkgroepen aan de gang, die onder de noemer van “Semantische interoperabiliteit” veel papier publiceren. (Wie op deze blog reageert laat zien dat er tenminste iemand is die dit leest....  Al doe je alleen maar: Like!)

Merkwaardig genoeg heeft de wetenschap de antwoorden al jarenlang op de plank liggen. Theorie, die wacht op toepassing. Ik heb dat recentelijk mogen doen voor de rechtspraak, en het werkt! Eén gedeelde waarheid, door en voor alle systemen. Dat kon zelfs zonder grote IT-projecten te lanceren! Mij dunkt, een goede aanleiding om nu eens wat belastinggeld te gaan besparen!

De faculteit Informatica heeft Sylvia Stuurman genomineerd als kandidaat voor de titel Docent van het Jaar 2011.

Sylvia Stuurman heeft in 2011 zeer bijzondere prestaties geleverd op het gebied van onderwijsvernieuwing.

Binnen het pilotproject OpenU Informatica heeft zij het eerste Hot topic van Informatica verzorgd en daarvan afgeleid een Opener cursus Scala gemaakt. Zowel het begrip hot topic als deze wijze van cursusontwikkeling: cursusontwikkeling in the cloud: samen met experts uit het veld een cursus ontwikkelen, zijn nieuw.

Het onderwerp van het Hot topic ontstond in een leesgroep van het domein Software technologie, waartoe Sylvia behoort. Op de TouWdag (een dag georganiseerd door de faculteit samen met de studievereniging) in maart 2011 gaf Sylvia een college en een workshop waaraan circa 50 Informaticastudenten enthousiast deelnamen. De literatuur en de presentatie vormden het startpunt van het hot topic, daarna werd het aangevuld met blogs, discussie en nog meer kennis tot het uiteindelijk in de vorm van een Openercursus uitkristalliseerde.

Omdat de faciliteiten van OpenU tijdens het project bedacht en ontwikkeld worden, is een andere, zelfs faculteitsoverstijgende, bijdrage van Sylvia aan het project OpenU het deelnemen namens onze faculteit door Sylvia aan het overleg met de ontwikkelaars. Door haar grote vakkennis  op het gebied van softwaretechnologie en haar goede communicatieve vaardigheden is zij een trait d’union tussen de verschillende stakeholders in het project: zij legt in begrijpelijke taal uit wat de techniek voor interessants kan en doet en denkt mee met de ontwikkelaars om de functionele wensen om te zetten in technische hoogstandjes.

Ook is zij een van de stuwende krachten achter het gebruik van sociale media in de faculteit en haar onderwijs, door haar "recepten" en voorbeelden trekt zij anderen over de streep om ermee aan de slag te gaan.

Met betrekking tot onderwijsontwikkeling is Sylvia de geestelijke moeder en belangrijkste auteur en begeleider van de cursus Webapplicaties: de clientkant. De Open Universiteit onderscheidt zich van andere universiteiten om in een dergelijk nieuw vakgebied een cursus aan te bieden. Dat er vraag naar is in de markt blijkt uit de belangstelling voor het Certified Professional Program Gecertificeerd Web application developer waar die cursus deel van uitmaakt. De masterstudent in onze commissie vond vooral de zeer zorgvuldige en opbouwende feedback die Sylvia op werkstukken geeft, zeer plezierig. Andere collega’s gebruiken Sylvia’s aanpak als voorbeeld voor hun werkwijze, onder andere haar beoordelingsformulieren voor de academische competenties bij de verdiepingsopdracht bij haar cursus Design Patterns. Ook noemen de studenten dat zij een bindende persoonlijkheid is, waar de collega’s het helemaal mee eens zijn.

Sylvia is tevens medeauteur en examinator van Software architecture en Requirements engineering en zij doet in het kader van de Free Technology Academy de begeleiding wereldwijd van de FTA-cursussen Software architecture en Web Application Development.

Net als voorgaande jaren bestond de commissie die de nominatie voorbereidde uit een gevorderde bachelor- en masterstudent en de opleidingsmanagers bachelor en master. Eén van de studenten maakte vorig jaar ook deel uit van de commissie. Daardoor wordt een gezamenlijk geheugen gewaarborgd.

Samenstelling van de commissie:

Hieke Keuning, masterstudent

Michallis Pashidis, bachelorstudent, lid FOC, maakte in 2010 ook deel uit van de commissie

Frank Wester, opleidingsdirecteur bachelor

Anda Counotte, opleidingsmanager master.

Second International Conference on Interactive Theorem Proving Berg en Dal, August 22-27 2011

Zaterdag 27 augustus was de laatste dag van het door de OU mede georganiseerde ITP congres. Met 120 deelnemers, 6 workshops, en 4 dagen van onderzoekspresentaties, invited lectures, en system demo's  is ITP 2011 een groot succes. Deelnemers kwamen vanuit de hele werld: australia, china, USA, en van oost, west en noord europa.

Mike Kishinevsky van Intel Corp. heeft het congres geopend met een overzicht van de uitdagingen in de verificatie van de communicatiearchitectuur van Intel's microprocessoren. Op dinsdag heeft Don Batory, hoogleraar van de University of Texas at Austin, ons verteld over het formeel bewijzen van software product lines. Dit is een nieuw en interessant onderwerp. Op woensdag heeft Bart Jacobs, hoogleraar van de Radboud Universiteit Nijmegen, het verhaal rond de OV chipkart uitgelegd. Zijn keynote heeft richtingen geven in het toepassen van formele methoden in het gebied van computer security. Als laatste invited speaker was Georges Gonthier van Microsoft Research aan de beurt. Hij heeft een overzicht gegeven over het formeel bewijzen van het Odd Order Theorem. Dit is een groot project dat een groot deel van algebra formeel gaat bewezen. Het success van dit project zal een belangrijke contributie zijn tot het formalizeren van wiskunde.

Op maandag heeft Warren Hunt laten zien hoe ACL2 in het ontwikkelproces van Centaur is gekomen. Dit is gezamenlijk werk met Anna Slobodova, Jared Davis, en Sol Swords. Op dinsdag hebben Wolfgang Ahrendt, Bernard Beckert, Richard Bubel, en Peter H. Schmitt details over het KeY systeem gegeven. KeY is ontwikkeld voor de verificatie van  Java programma's. In veel gevallen kunnen daarmee eigenschappen volledig automatich bewezen worden.

Tijdens het congres waren er 10 sessies waar onderzoekers over hun resultaten een presentatie hebben gegeven. Er waren 3 sessies over het formalizeren van wiskunde, en 2 sessies over software en hardware verificatie. De andere sessies waren over proof tools, nieuwe toepassingen, en het valideren van quantified Boolean formulas.

Na de ITP congres waren er 2 workshopdagen (vrijdag en zaterdag). In totaal waren er 6 workshops. Workshops hadden een bijzonder programma met interessant invited keynotes, o.a. van Henk Barendregt, Peter Sewell, Joseph Corneli, Edwin Brady, Marieke Huisman.

Het was een drukke week ! De deelnemers waren erg blij met het congres. De organisatie is ook heel tevreden.

Volgende jaar vindt ITP2011 in Princeton, USA plaats.

De OU heeft in belangrijke mate bijgedragen aan een internationaal congres over software correctheid. Onderzoekers Julien Schmalz en ikzelf vanuit de OU en Herman Geuvers en Freek Wiedijk vanuit de Radboud Universiteit Nijmegen organiseren samen het ITP (Interactive Theorem Proving) congres."

Iets dergelijks is eerder bij de mededelingen van de faculteit te lezen geweest. Dit congres is nu in volle gang. Het doel van theorem proving is te bewijzen dat software aan de specficatie voldoet. Die bewijzen worden mechanisch gecontroleerd dus dat levert de hoogste graad van betrouwbaarheid die maar mogelijk is.

Er zijn ongeveer 120 deelnemers vanuit de hele wereld, universiteiten en bedrijfsleven, die nadenken over programmas in allerlei programmeertalen (o.a. Java) en manieren om beter/makkelijker/sneller te kunnen bewijzen dat er geen fouten in zitten.

Als iedereen weer terug thuis is, zal software dan geen fouten meer bevatten?

Nee, zo snel gaat dat natuurlijk niet. Maar een bedrijf als Intel past deze technieken al wel toe in haar chip-design. Sinds ze een aantal jaren geleden honderden miljoenen (!) dollars kwijt waren aan de befaamde Pentium bug, is Intel erg actief in het gebruik van technieken om correctheid aan te tonen. Het kost echter nog veel werk om te doen en voor echt grote programmas is het eenvoudigweg te veel werk om aan te beginnen, maar een deel van een programma correct bewijzen is niet zo heel uitzonderlijk meer. Dit gebeurt echter alleen nog voor applicaties waarbij de schade veroorzaakt door fouten erg groot zou zijn. Aan het verbeteren van de correctheid van software draagt de OU via het onderzoek en het organiseren van dit congres haar steentje bij!

Sommigen van ons werken in een grote organisatie, waarin informatiesystemen het dagelijks werk ondersteunen. Zelf werk ik bijvoorbeeld (via Ordina) geregeld bij overheden, maar onze studenten werken natuurlijk overal....  De OU is trouwens een goed voorbeeld van een organisatie waarin veel IT wordt gebruikt: studienet, studentregistraties, financiele systemen, voorraadbeheer, noem maar op.

Maar werken al die systemen nu samen? Dat blijkt niet altijd het geval. Ook niet op de OU. En als u zelf in zo'n organisatie werkt, kent u wellicht voorbeelden uit eigen ervaring. En dat is gek, want we gebruiken service-orientatie, servicebussen, open protocollen, en allerlei andere maatregelen om de applicaties met elkaar te laten praten. Waarom kan een student zijn studievoortgang dan zo lastig volgen? En waarom kloppen gegevens uit het ene systeem niet altijd met het andere?

Het antwoord zit in de communicatie. Je kunt wel een protocol tussen applicaties standaardiseren, maar dan weet je nog steeds niet of de applicaties elkaar snappen. Je moet niet alleen de vorm (syntax) van de communicatie, maar ook de betekenis (semantiek) afspreken. En dat gebeurt niet altijd. Voor mensen is het al een hele uitdaging om elkaar te snappen, maar wij kunnen nog wel eens de bedoeling raden. Maar computers kunnen dat niet. Voor computers moet de betekenis van taal dus  nog veel preciezer worden gedefinieerd.

Best gaaf eigenlijk dat dat tegenwoordig kan. We kunnen betekenis in taal formeel definieren. Dat vereenvoudigt applicaties, en niet zo zuinig ook. Als we bijvoorbeeld het begrip "student" goed definieren, dan kunnen we immers volstaan met één systeem om de gegevens van studenten goed in op te slaan. Datzelfde geldt dan voor cursussen, tentamens, medewerkers, betalingen, en noem maar op. Geen dubbele opslag van gegevens betekent ook: geen inconsistentie in de systemen. Ik word helemaal warm en enthousiast van het vooruitzicht dat IT wél goed kan werken in de praktijk....