< Terug naar vorige pagina

Project

Een model-gebaseerde aanpak voor het ontwikkelen van zelf-adaptieve systemen met garanties

Moderne software systemen zijn in toenemende mate onderhevig aan onzekerheden die vaak moeilijk te voorspellen zijn tijdens de ontwikkeling. Voorbeelden zijn wijzigingen in de context waarin systemen uitvoeren en veranderingen in de beschikbaarheid van noodzakelijke diensten. Om de vereiste kwaliteiten te kunnen waarborgen (betrouwbaarheid, prestaties, e.d.) dient de software met de onzekerheden om te gaan tijdens de uitvoering. Een zelf-adaptief systeem maakt gebruik van een feedback-lus om zichzelf en de omgeving voortdurend te monitoren en zich aan te passen aan veranderingen om belangrijke kwaliteiten (aanpassingsdoelen) te garanderen. In het huidige onderzoek worden formele verificatietechnieken toegepast om garanties te bieden voor de aanpassingsdoelen tijdens de uitvoering. Hoewel deze technieken strikte garanties kunnen bieden zijn ze beperkt vanwege het bekende toestands-explosieprobleem. In dit proefschrift bestuderen we garanties voor zelf-adaptieve systemen vanuit een breder perspectief, met name: (1) functionele correctheid van de feedback-lus en (2) het garanderen van de aanpassingsdoelstellingen op een efficiënte manier. Daartoe stellen we ActivFORMS voor (Active FORmal Models for Self-adaptation), een formele, modelgedreven aanpak voor het ontwerp van zelf-adaptieve systemen met garanties. ActivFORMS garandeert functionele correctheid van de feedback-lus via directe uitvoering van formeel geverifieerde modellen van de feedback-lus met behulp van een herbruikbare virtuele machine. Daarnaast past ActiveFORMS statistische modelverificatie toe tijdens de uitvoering om op een efficiënte manier garanties te bieden voor de aanpassingsdoelen met voldoende betrouwbaarheid. ActivFORMS ondersteunt dynamische veranderingen van aanpassingsdoelen en updates van de geverifieerde feedback-lusmodellen. Om de brede toepasbaarheid en efficiëntie van de aanpak te demonstreren hebben we ActivFORMS in verschillende applicatiedomeinen geëvalueerd: magazijntransport, oceaanobservatie, tele-hulp en beveiligingsbewaking van gebouwen.

Datum:27 sep 2017 →  18 dec 2017
Trefwoorden:Executable models, MAPE-K feedback loop, Self-adaptive software systems, Statistical model checking, Formal methods
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