< Terug naar vorige pagina

Project

Van bedrijfsregels naar logica

In sommige industrieën, zoals de medische wereld of luchtvaart, kunnen storingen
tot onaanvaardbaar verlies leiden. Om veiligheid te garanderen, zijn er controles
ingebouwd voor iedere stap in het proces zoals standaarden, certifiëring, testen,
onderhoud. . . Voor software omvat dit een waaier aan benaderingen, onder
meer geautomatiseerd testen, veiligere programmeertalen, declaratieve talen die
kennis van uitvoering scheiding, alsook het genereren van bewijsbaar correcte
software op basis van een formele beschrijving van verwacht gedrag.
Deze thesis bevindt zich in de domeinen die de laatste twee ideën verkennen:
Kennis Representatie en Redeneren (KRR) en Formele Verificatie (FV). KRRonderzoekt hoe kennis kan voorgesteld worden met het oog op maximaal
menselijk begrip terwijl het (geautomatiseerd) redeneren met deze kennis
behouden blijft. Formele Verificatie focust op het modelleren van systeemgedrag
en de verificatie van juist gedrag in alle scenario’s.
Eén techniek die KRR gebruikt voor redeneertaken te verbeteren, zijn
justificaties (‘justifications’). Een justificatie, vaak voorgesteld als een
grafe, bevat een logboek hoe gevolgen afgeleid werden. Op deze manier
kunnen eenvoudig de ongesubstantieerde gevolgen gevonden worden wanneer
veronderstellingen ongeldig blijken. Deze tekst verkend hoe het gebruik
van justificaties oplossings-algoritmen voor pariteitsspellen vereenvoudigd.
Pariteitsspellen spelen een centrale role in Formele Verificatie. Het is een
oneindig twee-speler spel gespeeld op een gerichte grafe. Het inherente probleem
van een pariteitsspel bestaat uit de winnaars van de bepaalde knopen te bepalen,
met een bijhorende winnende strategie. Een oplossing van een pariteitsspel
wordt gebruikt om te bepalen of een implementatie voldoet aan de regels of
zelfs voor het opstellen van een correcte implementatie.
Concreet worden justificaties eerst aangepast voor gebruik in pariteitsspellen:
De vorm van een justificatie wordt gedefinieerd en samen met een operatie
Justify om justificaties te manipuleren. Aan de hand van deze operatie
worden vier bekende recursieve algoritmen gereconstrueerd. Deze varianten
werden geïmplementeerd en experimenteel geëvalueerd. De resultaten van deze
experimenten tonen hoe het gebruik van justificaties de huidige beste oplossers
versnelt. Tenslotte bewijzen we een equivalentie tussen pariteitsspellen en
geneste vastepunts definities, een oudere logica met andere toepassingen.

Datum:2 sep 2014 →  3 mei 2021
Trefwoorden:Business rule systems
Disciplines:Toegepaste wiskunde, Computerarchitectuur en -netwerken, Distributed computing, Informatiewetenschappen, Informatiesystemen, Programmeertalen, Scientific computing, Theoretische informatica, Visual computing, Andere informatie- en computerwetenschappen
Project type:PhD project