EVEREST: Nagenoeg volledige automatische verificatie voor geo-gerepliceerde systemen

Projectdetails

!!Description

Moderne gedistribueerde systemen repliceren informatie om hun algemene beschikbaarheid en
schaalbaarheid te verbeteren. Replicatie verhoogt echter systeemcomplexiteit, aangezien dat het
consistent houden van replica’s niet triviaal is. Als gevolg van het CAP theorema is veel onderzoek
gericht op het ontwikkelen van sterk consistente of eventuel consistente abstracties. Om de
correctheid van deze abstracties te garanderen, zijn onderzoekers afhankelijk van formele
specificaties met handmatige bewijzen. Onlangs zijn verificatietechnieken voorgesteld om dit te
verbeteren via bewijsassistentprogrammas. Deze technieken maken echter gebruik van abstracte
specificaties die losstaan van feitelijke implementaties en die aanzienlijke expertise vereisen voor
correct gebruik.
Om de ontwikkeling van geo-gerepliceerde systemen te vereenvoudigen, nemen wij een radicaal
nieuwe aanpak om de programmeerinspanning die nodig is om de juistheid van gedistribueerde
abstracties te verifiëren te verminderen. We bestuderen een nieuwe taal die constructies aanbied
voor de automatische verificatie van zulke abstracties. Via ondersteuning voor het afleiden van door
de gebruiker gedefinieerde metadata (bv. axiomen) kunnen we de verificatie optimaliseren en bij
sturen wanneer volledige automatisering niet mogelijk is, bv. voor recursieve datastructuren. Onze
aanpak heeft het potentieel om ontwikkelaars fundamenteel correcte abstracties te laten bouwen
zonder dat daarvoor aparte specificaties nodig zijn
AcroniemFWOAL1104
StatusActief
Effectieve start/einddatum1/01/2431/12/27

Keywords

  • programmeertalen
  • programmaverificatie
  • geo-gerepliceerde systemen

Flemish discipline codes in use since 2023

  • Language design, constructs and features
  • Coding tools and techniques, testing and debugging
  • Distributed systems
  • Programming languages and technologies

Vingerafdruk

Verken de onderzoeksgebieden die bij dit project aan de orde zijn gekomen. Deze labels worden gegenereerd op basis van de onderliggende prijzen/beurzen. Samen vormen ze een unieke vingerafdruk.