Hoe Werkt het MESON Bewijs en de RISC ProgramExplorer in RISCAL?

De Z3 solver is een handig hulpmiddel voor formele verificatie van wiskundige stellingen en programma's. Echter, de output die Z3 genereert is vaak moeilijk te interpreteren voor een mens, wat het lastig maakt om te begrijpen waarom een stelling waar is. Bovendien geeft Z3 geen aanwijzingen waarom een bewijs is mislukt. Deze tekortkomingen worden deels opgelost door de interne bewijsbeverwerker van RISCTP, waarvan de kern is gebaseerd op de bewijsstrategie MESON (Model Elimination, Subgoal-Oriented).

Bij het gebruik van RISCTP wordt de optie “Method MESON” geselecteerd in het RISCAL-menu onder “TP”. Vervolgens kunnen we, door in het pop-upmenu van de taakmap de optie “Apply Theorem Prover to All Theorems” te kiezen, dezelfde stellingen bewijzen die ook door Z3 werden getest. Door de optie “Print Theorem Prover Output” te kiezen, kunnen we de vertaling van een stelling van RISCAL naar RISCTP en de werking van de bewijsbeverwerker onderzoeken.

In tegenstelling tot externe bewijzers zoals Z3, produceert de interne MESON-beweisbeverwerker daadwerkelijk een bewijs dat begrijpelijker is voor de mens. Dit bewijs kan worden onderzocht door de optie “Open Theorem Prover GUI” te selecteren in het menu van de verificatieconditie “Is result correct?”. Er verschijnt een grafische interface waarin het bewijs wordt gepresenteerd als een geneste boomstructuur die de vereenvoudiging van het bewijsprobleem en de decompositie van het probleem in meerdere subproblemen toont, volgens de regels van de eerste-orde logica, aangevuld met verschillende rekenregels.

De subproblemen worden weergegeven onder de kop “Subproblems”, terwijl de vertaling naar een lagere vorm die de automatische werking van de MESON-bewijsbeverwerker mogelijk maakt, te vinden is onder “Clause Forms”. De bewijzen van de subproblemen worden getoond onder de kop “Proofs” als geneste mappen. Elke map vertegenwoordigt een bewijsopstelling gegenereerd door de bewijzer. Door op een bewijsopstelling te klikken, wordt een gedetailleerde uitleg getoond over hoe het bewijs in eenvoudiger subopstellingen wordt opgesplitst of uiteindelijk wordt afgebroken, hetzij door de MESON-beweisbeverwerker zelf, hetzij door een externe SMT-oplosser.

Deze manier van werken biedt niet alleen de mogelijkheid om succesvolle bewijzen in detail te onderzoeken, maar maakt het ook mogelijk om mislukte bewijzen te analyseren. Onder de kop “Proof Search” kunnen we zelfs mislukte bewijspogingen bekijken, die inzichten kunnen bieden over waarom een veronderstelde stelling niet bewezen kan worden. Dit kan waardevolle informatie opleveren voor verder onderzoek of het aanpassen van de oorspronkelijke stelling.

In de praktijk is de werking van de RISCTP interne bewijzer behoorlijk complex en een diepgaande uitleg valt buiten het bestek van deze introductie. Voor meer gedetailleerde informatie wordt verwezen naar [174].

Wanneer de RISC ProgramExplorer wordt opgestart, verschijnt een venster waarin een lijst van alle Java-bestanden en klassen in de huidige werkdirectory wordt weergegeven. Door dubbel te klikken op de klasse “Prog” wordt het bestand “Prog.java” geladen en semantisch verwerkt. In het midden van het venster bevindt zich een editor die de inhoud van het bestand toont, waarbij alle formele annotaties verborgen zijn. Door te klikken op een marker “+” in de linker balk, worden de betreffende annotaties in blauwe kleur getoond.

De klasse “Prog” bevat een statische Java-methode “search” die het lineaire zoekalgoritme implementeert, zoals beschreven in Sectie 8.1 en geverifieerd in Sectie 8.5. Deze methode bevat formele annotaties die de precondities en postcondities van de methode beschrijven. De preconditie vereist bijvoorbeeld dat de parameterarray a niet null is, terwijl de postconditie aangeeft dat de methode de index van een element x in de array retourneert, of -1 als x niet in de array voorkomt.

De annotaties worden als volgt gepresenteerd: /*@ requires (VAR a).null = FALSE; ensures LET result = VALUE@NEXT, n = (VAR a).length IN IF FORALL(k: INT): 0 <= k AND k < n => (VAR a).value[k] /= VAR x THEN result = -1 ELSE 0 <= result AND result < n AND (FORALL(k: INT): 0 <= k AND k < result => (VAR a).value[k] /= VAR x) AND (VAR a).value[result] = VAR x ENDIF; @*/. Deze annotaties worden vertaald naar een relationele semantiek in de RISC ProgramExplorer, waarbij de veranderingen in de toestand van de variabelen en hun afhankelijkheden tijdens de uitvoering van de methode worden aangegeven.

Een belangrijke eigenschap van de RISC ProgramExplorer is de mogelijkheid om de semantiek van elke commando in de methode te inspecteren. Dit gebeurt door de actieve labels in de linker panel te selecteren en de overeenkomstige transitierepresentatie van de toestand en de beëindigingsvoorwaarden te bekijken. In wezen biedt de RISC ProgramExplorer een gedetailleerd overzicht van hoe een Java-programma werkt, rekening houdend met de formele annotaties die de veronderstelde correctheid van het programma ondersteunen.

In de praktijk, wanneer een taak in de RISC ProgramExplorer wordt uitgevoerd, wordt de status van de bewijzen weergegeven met verschillende kleuren: blauw betekent dat de taak al automatisch is opgelost, paars betekent dat er al een bewijs is dat in een eerdere sessie is gegenereerd en rood geeft aan dat er nog geen geldig bewijs is. Dit stelt de gebruiker in staat om snel te zien welke taken nog moeten worden verwerkt en welke al gevalideerd zijn.

De integratie van formele methoden in de RISC ProgramExplorer biedt een krachtige manier om de correctheid van programma’s te waarborgen. Echter, het is belangrijk om te begrijpen dat formele verificatie niet altijd triviaal is. Het vereist een diepgaande kennis van de logica en de semantiek van de gebruikte programmeertaal, evenals een zorgvuldige formulering van de vereisten en garanties van het programma. Desondanks kan het proces waardevolle inzichten bieden en de betrouwbaarheid van software aanzienlijk verbeteren.

Hoe waarborgen we de veiligheid en eerlijkheid in gedistribueerde systemen met TLA+ en RISCAL?

In gedistribueerde systemen, vooral die waarbij meerdere clients toegang proberen te krijgen tot een gedeelde bron, is het essentieel om ervoor te zorgen dat de systeemstatus altijd geldig blijft en dat geen client oneindig wacht. Dit kan worden gemodelleerd en geverifieerd met behulp van de formalisme TLA+ en het modelleersysteem RISCAL, die beide krachtige hulpmiddelen bieden voor het analyseren van systemen op hun veiligheid en eerlijkheid.

Laten we eerst naar de systeemtransities kijken. Een typische transitie in TLA+ wordt beschreven door een predicaat dat de overgang van een systeemvariabele in de prestate naar de poststate vastlegt. Een voorbeeld hiervan is de overgang van een client 𝑖 die een verzoek doet om een gedeelde bron te verkrijgen. Deze transitie kan worden vastgelegd als volgt:

matlab
Copy code
RC(i) == \/ Goto(i,0,1) /\ Send(req,i) /\ ans’ = ans 
         \/ Goto(i,1,2) /\ Receive(ans,i) /\ req’ = req 
         \/ Goto(i,2,0) /\ Send(req,i) /\ ans’ = ans

In deze formule beschrijft RC(i) de mogelijke transities voor een client 𝑖, waarbij elke transitie de toestand van de client wijzigt afhankelijk van de interactie met de server. Het symbool ans’ geeft de waarde aan na de transitie, wat betekent dat de server de aangevraagde bron terugstuurt naar de client.

Evenzo kunnen we de overgang van de server beschrijven, die de berichten van de clients verwerkt en de bronnen aan hen toewijst. Dit kan bijvoorbeeld als volgt:

swift
Copy code
RS(i) == Receive(req,i) /\ RS0(i) /\ pc’ = pc

Hier wordt het ontvangen van een verzoek van een client beschreven, en de server verwerkt de aanvraag door de status van de systemvariabele pc te veranderen, afhankelijk van de interactie met de client.

Het systeem wordt nu gedefinieerd als een combinatie van transities van zowel clients als servers. Het belangrijkste predicaat voor het systeem kan als volgt worden beschreven:

ini
Copy code
ClientServer == I /\ [][R]_Vars

Dit geeft aan dat het systeem begint in de initiële toestand I, en dat elke stap van het systeem voldoet aan de transitievoorwaarden die zijn gedefinieerd door de relationele predicaten van de clients en de server. Het gebruik van "stuttering steps" in deze formule zorgt ervoor dat het systeem abstractere en concrete uitvoeringen van zijn stappen kan ondersteunen.

Nu we de transitie van het systeem hebben gedefinieerd, kunnen we de veiligheidseigenschappen controleren. Een belangrijke eigenschap is het MutEx-criterium, dat waarborgt dat geen twee clients gelijktijdig toegang krijgen tot de kritieke regio. Dit wordt als volgt gedefinieerd:

ini
Copy code
MutEx == \A i \in Clients, j \in Clients: i /= j => ~(pc[i] = 2 /\ pc[j] = 2)

Deze eigenschap garandeert dat wanneer een client in de kritieke regio is (pc[i] = 2), geen andere client tegelijkertijd deze regio kan betreden. Door gebruik te maken van de TLC Model Checker kunnen we deze eigenschap verifiëren, en de uitvoeringsresultaten van het model tonen aan of het systeem voldoet aan deze veiligheidseigenschap.

Naast veiligheid is het ook belangrijk om te zorgen voor liveness, oftewel dat het systeem geen client in een eeuwige wachttijd plaatst. Dit kan worden uitgedrukt door de NotStarve-eigenschap:

ini
Copy code
NotStarve == \A i \in Clients: pc[i] = 1 ~> pc[i] = 2

Deze eigenschap garandeert dat een client die een verzoek doet om toegang te krijgen tot de gedeelde bron uiteindelijk de bron krijgt. Als deze eigenschap echter niet zorgvuldig wordt geconfigureerd, kan het systeem vastlopen. Dit is precies wat gebeurde in het model waarbij, ondanks dat de server klaar was om een bericht te ontvangen, een bericht in de wachtrij bleef zonder ooit te worden verwerkt.

Om deze liveness-problemen op te lossen, moeten we eerlijkheidsvoorwaarden aan het systeem toevoegen. Dit kunnen we doen door het systeem te verfijnen met zwakke of sterke eerlijkheidseisen. Zwakke eerlijkheid zorgt ervoor dat elke client die klaar is om een stap te maken, deze uiteindelijk ook zal maken. Sterke eerlijkheid gaat nog verder door ervoor te zorgen dat een client die het verzoek doet om een bron te ontvangen, deze ook daadwerkelijk ontvangt, zelfs als andere clients de bron tijdelijk krijgen. In TLA+ kunnen deze voorwaarden worden geformuleerd als volgt:

ini
Copy code
ClientServer == I /\ [][R]_Vars /\ \A i \in Clients: WF_Vars(RC(i)) /\ WF_Vars(RS(i))

Met deze uitbreiding kunnen we garanderen dat elke client zijn verzoek uiteindelijk verwerkt krijgt. Echter, wanneer het systeem meer clients bevat, kunnen nieuwe problemen ontstaan. Als we bijvoorbeeld N=3 instellen, kan de verificatie van de liveness-eigenschap opnieuw een fout veroorzaken. Het systeem lijkt vast te lopen wanneer de toegang tot de bron wordt afgewisseld tussen twee clients, terwijl de derde client nooit de kans krijgt om toegang te krijgen.

Dit kan worden opgelost door de sterke eerlijkheidseisen verder uit te breiden. Deze uitbreiding garandeert dat als een client zijn verzoek heeft ingediend en het in de wachtrij van de server staat, de server dit verzoek uiteindelijk zal verwerken:

swift
Copy code
ClientServer == /\ I /\ [][R]_Vars /\ \A i \in Clients: WF_Vars(RC(i)) /\ WF_Vars(RS(i)) /\ \A g \in Clients: SF_Vars(\E i \in Clients: Receive(req,i) /\ i = given /\ GiveWaiting(g) /\ pc’ = pc)

Met deze aanpassing kunnen we zelfs voor grotere systemen zoals N=3 garanderen dat alle clients eerlijk behandeld worden en dat geen enkele client in een eindeloze wachttijd terechtkomt.

Bij het gebruik van RISCAL kunnen we vervolgens de systeemspecifieke modellen verifiëren, zoals we eerder deden met TLA+. In RISCAL worden de systemen gemodelleerd op een vergelijkbare manier als in TLA+, met behulp van specifieke axiomata en variabelen. Zo kunnen we de configuraties van de clients en hun bijbehorende acties in het systeem nauwkeurig volgen en controleren.