Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing

Dit artikel beschrijft de formele modellering, verificatie met Uppaal en testgeneratie voor de Contract Automata Runtime Environment (CARE), waarmee de betrouwbaarheid van deze gedistribueerde applicatie wordt versterkt.

De kern

De Digitale Regisseur en zijn Onzichtbare Regels: Een Verhaal over CARE

Stel je voor dat je een groot orkest hebt met tientallen muzikanten (de diensten). Iedereen speelt een ander instrument, maar ze moeten perfect samenwerken om een symfonie te spelen. De uitdaging? Ze zitten niet in dezelfde kamer; ze communiceren via telefoonlijnen (het internet) en ze hebben allemaal hun eigen manier van noteren.

Om ervoor te zorgen dat ze niet in de war raken en dat iedereen op het juiste moment zijn noot speelt, heb je een regisseur nodig. In de wereld van computersoftware heet dit de Contract Automata Runtime Environment (CARE). CARE is die regisseur die zorgt dat de verschillende computerprogramma's netjes met elkaar praten.

Maar hoe weet je of die regisseur zijn werk goed doet? Wat als hij per ongeluk een fout maakt en de hele symfonie vastloopt (een deadlock)? Of wat als hij een briefje verliest dat hij naar een muzikant moet sturen?

In dit artikel vertelt de auteur, Davide Basile, hoe hij deze regisseur (CARE) heeft onderzocht met een heel speciale bril: formele methoden. Laten we dit verhaal in drie simpele hoofdstukken vertellen.

1. De Blauwdruk: Het Tekenen van de Regisseur

Eerst heeft de auteur de regisseur niet gewoon "gekeken", maar hem getekend. Hij heeft een heel precies, wiskundig model gemaakt van hoe CARE werkt.

• De Analogie: Stel je voor dat je een heel ingewikkeld bordspel wilt bouwen. In plaats van het spel direct te spelen en te hopen dat het werkt, teken je eerst elke mogelijke zet, elke regel en elke reactie op papier.
• Wat deed hij? Hij gebruikte een softwaretool genaamd UPPAAL. Dit is als een superkrachtige simulator die kan zien of je bordspel ooit vastloopt. Hij heeft CARE omgezet in een netwerk van "tijdsautomaten". Dat klinkt ingewikkeld, maar het is eigenlijk gewoon een gedetailleerde flowchart die laat zien: "Als A een bericht stuurt, moet B wachten tot de buffer niet vol is, en dan antwoordt C."

2. De Proef: De Regisseur op de Helling

Nu de blauwdruk klaar was, ging de echte test beginnen. De auteur gebruikte UPPAAL om twee dingen te doen:

A. De "Wat als?"-testen (Verificatie)
Hij vroeg de computer: "Wat gebeurt er als we 100 muzikanten hebben en de telefoonlijnen zijn traag?" of "Wat als de regisseur een bericht vergeet?"

• Het resultaat: De computer draaide miljoenen simulaties. Hij zocht naar de ergste scenario's.
• De ontdekking: Tijdens het tekenen van het model ontdekte de auteur een fout in de echte software die niemand eerder had gezien! In de echte code wachtte de regisseur op een antwoord van iedereen, zelfs van muzikanten die niet hoefden te spelen. Dit zou de hele symfonie laten vastlopen. Omdat hij dit in het model zag, kon hij de code voor het probleem zich echt voordoet, repareren.

B. De "Statistische" test
Soms is het onmogelijk om alles te testen (te veel combinaties). Dus gebruikte hij een statistische methode: "Laten we 10.000 keer snel spelen en kijken hoe vaak er iets misgaat."

• De uitkomst: Het bleek dat de kans op een vastlopend systeem of verloren berichten extreem klein was, zolang de instellingen (zoals de grootte van de wachtrijen) maar goed stonden. Dit gaf hem vertrouwen dat CARE betrouwbaar is.

3. De Bril: Van Theorie naar Praktijk (Testen)

Dit is het meest interessante deel. Vaak maken mensen een mooi model, maar vergeleken ze dit nooit met de echte code. Hier deed de auteur iets unieks:

Hij gebruikte het model om automatisch testjes te schrijven voor de echte software.

• De Analogie: Stel je hebt een model van een auto. In plaats van zelf te raden wat je moet testen, laat je het model een route plotten: "Eerst remmen, dan sturen, dan gas geven." Vervolgens neemt de computer die route en voert hij hem letterlijk uit op de echte auto om te zien of hij doet wat het model zegt.
• Hoe werkte het? De computer las het model, zag een specifieke route (bijvoorbeeld: "Regisseur vraagt om koffie, Bob biedt koffie aan, Alice vraagt suiker"), en schreef daar direct een testcode voor in Java (het taal van CARE).
• Het resultaat: Deze automatisch gegenereerde tests werden uitgevoerd op de echte CARE-software. Ze bleken perfect te werken. Dit bewees dat het model niet te abstract was; het was een eerlijke weergave van de werkelijkheid.

Waarom is dit belangrijk?

De auteur laat zien dat je niet hoeft te wachten tot een softwarefout zich voordoet in de echte wereld (waarbij geld verloren gaat of systemen crasht).

1. Betrouwbaarheid: Door eerst het model te "spelen" met de computer, kun je fouten vinden die mensen over het hoofd zien.
2. Vertrouwen: Omdat de tests uit het model kwamen en op de echte code werkten, weten we nu zeker dat CARE doet wat hij moet doen.
3. Transparantie: Het model fungeert als een duidelijke handleiding. In plaats van 770 regels code te lezen, kun je de flowchart bekijken om te begrijpen hoe het systeem werkt.

Kortom:
Deze paper is het verhaal van iemand die een complexe digitale regisseur (CARE) heeft getekend, gecontroleerd op fouten met een supercomputer, en vervolgens die tekening heeft gebruikt om de regisseur te trainen. Het resultaat? Een software-systeem dat niet alleen werkt, maar waarvan we weten dat het werkt, zelfs in de ergste situaties. Het is als het bouwen van een brug, waarbij je eerst een perfect model bouwt om te zien of hij in een orkaan blijft staan, voordat je ook maar één steen legt.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing" in het Nederlands.

Probleemstelling

Het artikel richt zich op de Contract Automata Runtime Environment (CARE), een gedistribueerde middleware-toepassing die is ontworpen om servicespecifcaties, gedefinieerd via contractautomata, te realiseren. Hoewel de algoritmen voor de synthese van orkestraties in CARE wiskundig bewezen correct zijn, bestaat er een risico dat de lage-niveau implementatie (communicatie via Java TCP/IP sockets, bufferbeheer, en interacties tussen de orkestrator en services) fouten bevat die niet door de formele specificatie worden gedekt.

In de praktijk kunnen correcte algoritmen falen door implementatieproblemen zoals deadlocks, verloren berichten of timing-issues. Het artikel identificeert het gebrek aan een directe link tussen abstracte formele modellen en de concrete broncode als een kritieke hiaat in de softwareontwikkeling, wat de betrouwbaarheid van open-source gedistribueerde systemen in gevaar brengt.

Methodologie

De auteurs hanteren een bottom-up benadering om CARE formeel te modelleren, te verifiëren en te testen. De kern van de methodologie omvat:

1. Formele Modellering (Stochastic Timed Automata):

   • De interacties van CARE worden gemodelleerd als een netwerk van stochastische getijdeautomaten (stochastic timed automata) in het Uppaal-toolset.
   • Abstrahering: De onderliggende applicatie (de daadwerkelijke business logica) wordt geabstraheerd. In plaats van de specifieke payload van berichten te modelleren, worden deze vervangen door probabilistische keuzes en abstracte constanten. Dit maakt het model schaalbaar en toepasbaar op elke geldige orkestratie.
   • Socket-communicatie: Java TCP/IP sockets (asynchroon met FIFO-buffers) worden gemodelleerd via globale arrays en wachtrijen. Blokkerende I/O-operaties worden gesimuleerd met exponentiële vertragingen. Een specifiek automaton (SocketTimeout) modelleert de timeout-mechanismen van Java-sockets om eindeloze wachttijden te voorkomen.
   • Configuraties: Het model ondersteunt verschillende configuraties voor keuzes (dictatoriaal vs. meerderheids) en acties (gecentraliseerd vs. gedistribueerd).

2. Verificatie (Model Checking):

   • Exhaustieve Model Checking: Gebruikt voor het bewijzen van veiligheids-eigenschappen (zoals afwezigheid van deadlocks en orphan messages) op kleinere instantiaties van het systeem.
   • Statistische Model Checking (SMC): Gebruikt voor het evalueren van kwantitatieve eigenschappen (bijv. waarschijnlijkheid van timeouts of bufferoverloop) op grotere systemen waar de toestandsruimte te groot is voor exhaustieve analyse.
   • Parameter Tuning: SMC wordt gebruikt om realistische parameters (buffergrootte, timeout-drempels, vertragingen) te bepalen die de werkelijkheid nabootsen zonder de state-space onnodig te vergroten.

3. Traceerbaarheid en Model-Based Testing:

   • Er wordt een directe link gelegd tussen de overgangen in het Uppaal-model en de specifieke regels in de Java-broncode (via commentaar in het model).
   • Testgeneratie: Uppaal's tool Yggdrasil genereert abstracte testgevallen (traces) op basis van bereikbaarheidsqueries (bijv. E<>).
   • Concretisatie: Deze abstracte tests worden automatisch omgezet in concrete JUnit-tests voor de Java-implementatie. De abstracte waarden worden vervangen door concrete waarden en assertions worden toegevoegd om de correctheid van de communicatie te verifiëren.

Belangrijkste Bijdragen

1. Bottom-up Formeel Model: Het eerste volledige formele model van een bestaande, open-source middleware (CARE) als een netwerk van stochastische getijdeautomaten.
2. Integratie van Verificatie en Testing: Een robuust raamwerk dat zowel exhaustieve als statistische verificatie combineert met model-based testing om de connectie tussen theorie en praktijk te versterken.
3. Traceerbaarheid: Een uniek mechanisme waarbij elke overgang in het formele model expliciet wordt gekoppeld aan de corresponderende regels in de Java-broncode, wat de validatie van het abstractieniveau mogelijk maakt.
4. Ontdekking en Correctie van Fouten: Het proces heeft concrete bugs in de implementatie van CARE blootgelegd (bijvoorbeeld een deadlock-situatie waarbij de orkestrator wachtte op antwoorden van services die niet betrokken waren bij een keuze), die vervolgens zijn gefixt.

Resultaten

• Verificatie van Eigenschappen: Het model heeft bewezen dat er geen deadlocks optreden (behalve bij onjuiste configuraties), dat er geen "orphan messages" (niet-geconsumeerde berichten) achterblijven in buffers bij voltooiing, en dat de orkestratie correct afloopt of een timeout genereert.
• Parameteroptimalisatie: Door middel van SMC is vastgesteld dat een buffergrootte van 5 en een timeout van 15 tijdseenheden een realistisch gedrag simuleren met een zeer lage waarschijnlijkheid van fouten (< 1%).
• Testdekking: De gegenereerde JUnit-tests dekken een significant deel van de broncode (zoals aangetoond door IntelliJ coverage rapporten). De tests valideren zowel de orkestrator als de services onder verschillende configuraties (dictatoriaal/majoritair, gecentraliseerd/distributed).
• Validatie van het Model: De hoge dekking van de tests bevestigt dat het abstracte model niet te grof is en de essentie van de implementatie correct weergeeft.

Betekenis en Impact

Dit onderzoek demonstreert de praktische waarde van formele methoden in de ontwikkeling van complexe, open-source gedistribueerde systemen. Het toont aan dat:

• Formele modellering niet alleen theoretisch nuttig is, maar ook concrete bugs in bestaande software kan opsporen die door traditionele testing zijn gemist.
• De combinatie van statistische en exhaustieve verificatie een balans biedt tussen diepgaande analyse en schaalbaarheid.
• Model-Based Testing een effectieve brug slaat tussen abstracte specificaties en concrete implementaties, waardoor de betrouwbaarheid van het systeem aanzienlijk wordt verhoogd.

De auteurs benadrukken dat dit werk een stap is naar een volledig model-gedreven ontwikkelproces, waarbij de kloof tussen ontwerpers en ontwikkelaars wordt overbrugd door traceerbaarheid en geautomatiseerde testgeneratie. Toekomstig werk richt zich op het automatiseren van de synchronisatie tussen model en code en het gebruik van nieuwe tools (zoals Uppex) om modelvarianten beter te beheren.