Promotie: obstakels weghalen in de ontwikkeling van gedistribueerde systemen

Blockchains en webapplicaties

Gedistribueerde systemen zijn niet meer weg te denken uit de moderne samenleving. Een gedistribueerd systeem is een softwaresysteem dat bestaat uit meerdere componenten die op verschillende machines worden uitgevoerd en berichten met elkaar uitwisselen via een netwerk. Webapplicaties, cloudtechnologie, en blockchains zijn enkele voorbeelden van gedistribueerde systemen.

Choreografieën

Het correct ontwerpen en implementeren van deze systemen is erg ingewikkeld. Een belangrijke reden hiervoor is het samenspel van de deelnemers in een systeem: bepaalde taken mogen gelijktijdig gebeuren, terwijl andere taken afhankelijk zijn van elkaar. Het coördineren van deelnemers vereist communicatie tussen hen, wat kan worden gespecificeerd door middel van communicatieprotocollen. Choreografieën zijn een specifieke notatie voor communicatieprotocollen, die ze specificeert vanuit een globaal perspectief, en die bepaalde wenselijke eigenschappen per constructie garandeert.

Communicatiepatronen

De communicatiepatronen hebben beperkingen. Edixhoven onderzoekt in zijn proefschrift manieren om deze beperkingen weg te nemen. Hij bestudeert hiervoor een bestaande operator uit de formeletalentheorie, met de naam 'shuffle on trajectories', en laat zien dat deze kan worden gebruikt in een choreografietaal om een grote gedragsklasse te specificeren, met behoud van wenselijke eigenschappen. Een tweede probleem is dat het onmogelijk kan zijn om bepaalde communicatiepatronen te implementeren op een manier die precies overeenkomt met een specificatie; we zeggen dan dat een specificatie niet realiseerbaar is. In het algemeen kost het bepalen van realiseerbaarheid exponentieel veel tijd of is het onbeslisbaar.

Nieuw model

Edixhoven introduceert als oplossing voor dit tweede probleem een nieuw model voor het gedrag van choreografieën, gebaseerd op partieel geordende verzamelingen: deze ‘vertakkende pomsets’ vormen een compact model voor combinaties van gelijktijdigheid en keuze, een typisch element van choreografieën. Vervolgens definieert hij structurele eisen op dit model die een conservatieve benadering geven van realiseerbaarheid. Het onderzoek van Edixhoven werd uitgevoerd aan de Open Universiteit, met ondersteuning van de onderzoeksschool IPA (Institute for Programming Research and Algorithmics). Delen van het onderzoek zijn uitgevoerd bij het Centrum Wiskunde & Informatica (CWI) en het Leiden Institute of Advanced Computer Science (LIACS) van de Universiteit Leiden.

Promotie Luc Edixhoven

Luc Edixhoven (1995, Rennes(FR)) is promovendus bij de faculteit Bètawetenschappen van de Open Universiteit. Hij verdedigt zijn proefschrift 'Expressive specification and verification of choreographies' op vrijdag 12 december 2024 om 13.30 uur aan de Open Universiteit in Heerlen. De promotores zijn dr. Bastiaan Heeren (Open Universiteit) en prof. dr. Marcello Bonsangue (Universiteit Leiden). De copromotor is dr. Sung-Shik Jongmans (Open Universiteit).

De promotie is live bij te wonen bij de Open Universiteit in Heerlen en kan online worden gevolgd via www.ou.nl/live.