Modulaire statische analyse voor de zachte verificatie van contracten in gedistribueerde actor programma's

Projectdetails

!!Description

Gedistribueerde programma’s, dewelke gevormd worden door
onafhankelijke systemen die met elkaar communiceren om een
gemeenschappelijk doel te bereiken, zijn alomtegenwoordig. Actors
voorzien een geschikt model om gedistribueerde systemen te
beschrijven en te implementeren. Jammer genoeg maken
programmeurs meer fouten in gedistribueerde programma’s dan
sequentiële programma’s. Dit komt onder andere doordat
programmeurs de moeilijkheden van gedistribueerde systemen
onderschatten. Design-by-contract blijkt een krachtig paradigma te
zijn waarmee het gewenste gedrag van een programma kan worden
beschreven, waardoor ze robuuster worden tegen fouten. Helaas
introduceert het naleven van deze contracten vaak een grote last
tijdens de uitvoer. Wij stellen een nieuwe contracten taal voor om het
gedrag van gedistribueerde actor programma’s mee te beschrijven.
Om de last bij het uitvoeren van het programma te verminderen en
om potentiële defecten op voorhand te kunnen detecteren stellen we
een zachte verificatie voor. Het doel van deze verificatie is om zoveel
mogelijk contract controles te verifiëren, en de niet geverifieerde
controles als residuen achter te laten en nog steeds bij de uitvoer te
controleren. Gedistribueerde programma’s zijn vaak moeilijker om
statisch te analyseren door het niet-determinisme van de
meervoudigheid van berichten, en gedeeltelijke falingen. We stellen
een proces modulaire analyse voor om de verificatie schaalbaar,
maar ook voldoende precies te houden
AcroniemFWOTM1089
StatusActief
Effectieve start/einddatum1/11/21 → 31/10/25

Keywords

  • gedistribueerde programmaverificatie
  • ontwerp-door-contract
  • statische analyse

Flemish discipline codes in use since 2023

  • Computer science

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.
Volledige vingerafdruk bekijken
  • 3 Conference paper

  • Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts

    Vandenbogaerde, B., Stiévenart, Q. & De Roover, C., 15 aug 2024, Proceedings of the ACM on Programming Languages. ICFP redactie ACM, Vol. 8. blz. 515-543 29 blz. 254. (Proceedings of the ACM on Programming Languages; vol. 8, nr. ICFP).

    Onderzoeksoutput: Conference paper

    Open Access
    Bestand
    1 Citaat (Scopus)
    11 Downloads (Pure)

  • Cross-Level Debugging for Static Analysers

    Van Molle, M., Vandenbogaerde, B. & De Roover, C., 23 okt 2023, Proceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering (SLE ’23): SPLASH 2023. Saraiva, J., Degueule, T. & Scott, E. (redactie). New York, NY, USA: ACM, blz. 138-148 11 blz. (SLE 2023 - Proceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering, Co-located with: SPLASH 2023).

    Onderzoeksoutput: Conference paper

    Open Access
    Bestand
    1 Citaat (Scopus)
    53 Downloads (Pure)

  • Summary-Based Compositional Analysis for Soft Contract Verification

    Vandenbogaerde, B., Stiévenart, Q. & De Roover, C., 2022, Proceedings - 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation, SCAM 2022: 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM). 22 redactie IEEE, blz. 186-196 11 blz. (Proceedings - 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation, SCAM 2022).

    Onderzoeksoutput: Conference paper

    Open Access
    Bestand
    3 Citaten (Scopus)
    62 Downloads (Pure)
  • 2 Talk or presentation at a conference