Over ons onderzoek

Het masterprogramma Computing Science wordt aangeboden in nauwe samenwerking met het Institute for Computing and Information Sciences (iCIS). De specialisatie Softwarewetenschap bouwt voort op de sterke internationale reputatie van iCIS op gebieden zoals modelgebaseerd testen, virtuele productontwikkeling, geavanceerd programmeren en domeinspecifieke talen.

Onderzoeksinstituten

Institute for Computing and Information Sciences

Het algemene doel van iCIS is het verbeteren van de beveiliging en betrouwbaarheid van computergebaseerde systemen en algoritmen op basis van wiskundig onderbouwde theorieën. Door middel van baanbrekend onderzoek is iCIS een pionier op het gebied van onderzoek en draagt het bij aan de samenleving, vooral op het gebied van cyberbeveiliging. iCIS kijkt verder dan zijn eigen vakgebied door knowhow te integreren met andere disciplines zoals recht, geneeskunde en neurowetenschappen. Door deze aanpak is iCIS niet alleen relevant in onderzoek, maar pakt het ook de uitdagingen van IT in de moderne samenleving aan.

Onderzoek bij iCIS is georganiseerd in drie verschillende onderzoeksafdelingen:

Softwarewetenschap
Digitale beveiliging
Datawetenschap

Onderzoeksgroepen

Software Science

De onderzoeksgroep Software Science bij iCIS heeft expertise op een breed scala van onderwerpen met betrekking tot softwareconstructie en -analyse. Onze groep is bekend om onderzoek naar:

model learning, modelgebaseerd testen en model checking
programma-verificatie met behulp van proof assistants
combinatie van formele verificatie en machine learning
model based software-engineering
domeinspecifieke talen
functioneel programmeren en HPC/array computing
wiskundige fundamenten van software: type theory, concurrency theory, co-algebras, en term rewriting

Hoewel we tijdens de masterspecialisatie het gehele veld van Software Science bestuderen, leggen we meer nadruk op en zijn we gespecialiseerd in een aantal gebieden:

Domeinspecifieke talen

De 'Holy Grail' waar we naar op zoek zijn, is de mogelijkheid om een volledig functioneel systeem volledig automatisch uit een model te genereren, met als doel de softwareontwikkeltijd te verkorten en de systeembetrouwbaarheid te verhogen. Dit is in het algemeen heel moeilijk te bereiken, maar voor specifieke probleemgebieden zou het mogelijk moeten zijn. Idealiter wil je een systeem specificeren tot een niveau van abstractie dat gemakkelijk te begrijpen is door domeinspecialisten. Hiervoor leren we onze studenten hoe ze een domeinspecifieke taal moeten gebruiken.

Automata learning

Automatenleren (ook wel Model Learning genoemd) komt op als een zeer effectieve techniek voor het verkrijgen van black-box toestandsmodellen van softwaresystemen, en heeft bewezen zeer effectief te zijn in het vinden van bugs in software-implementaties. Het doel van automata learning is het verkrijgen van een state model van een systeem door invoer te geven aan en uitvoer te observeren van een black-box systeem. De Radboud Universiteit is internationaal leidend in dit nieuwe gebied, door theoretische vooruitgangen, toolontwikkeling en toepassingen in gebieden zoals netwerkprotocollen, bankpassen en legacy-software. Bekijk de video om meer te leren over ons onderzoek naar Model Learning.

Model based testing

Systematisch testen is belangrijk voor de softwarekwaliteit, maar het is ook foutgevoelig, kostbaar en tijdrovend. Model based testing is een effectieve en efficiënte testmethode die wordt gebruikt om te bewijzen dat een systeem voldoet aan de eisen die eraan worden gesteld. Een model vormt het uitgangspunt voor testen. Dit model drukt precies en volledig uit wat een systeem onder test moet doen en wat niet, en vormt daardoor een goede basis voor het systematisch genereren van testgevallen. Dit is een interessant gebied waarin we zowel met de Cyber Security-groep samenwerken om modellen van beveiligingsprotocollen te leren kennen, als met de Mathematical Foundations-groep over de onderliggende theorie.

Taakgeoriënteerd en functioneel programmeren

Het idee is dat een computerprogramma een mens ondersteunt bij het uitvoeren van een bepaalde taak of autonoom een taak kan uitvoeren. Als we de taak die moet worden uitgevoerd precies kunnen definiëren, of een complexe taak kunnen verdelen in kleinere, eenvoudigere taken, zouden we voldoende informatie moeten hebben om een uitvoerbaar systeem uit de beschrijving te genereren dat het beschreven werk ondersteunt. Dit betekent dat alle technische infrastructuur van een interactief systeem (het verwerken van evenementen, het opslaan van gegevens, coderen/decoderen, enzovoort) kan worden verdeeld en op generieke wijze kan worden opgelost.

Met andere woorden, een programmeur kan zich nu richten op het belangrijkste probleem van welke taak moet worden ondersteund, zonder zich zorgen te maken over de technische details om het te laten functioneren.

Model checking

De betrouwbaarheid van digitale systemen kan niet langer voldoende worden gecontroleerd door traditionele benaderingen van testen en simulatie. Het is daarom essentieel om wiskundige modellen van deze systemen te bouwen en (algoritmische) verificatiemethoden te gebruiken om deze modellen te analyseren. Bij model checking worden specificaties over het systeem uitgedrukt als (tijd) logicaformules. Symbolische algoritmen worden gebruikt om het model te doorlopen dat door het systeem is gedefinieerd, en om te controleren of de specificatie al dan niet klopt. Aangezien model checking volledig automatisch is en geen complexe kennis van bewijsstrategieën of de vooringenomenheid van simulatiehulpmiddelen vereist, is het de methode bij uitstek voor verificatie op industriële schaal.