💻 computer science

Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

Dit artikel presenteert een techniek voor het compileren van het synchrone fragment van Signal Temporal Logic (SSTL) naar modulaire synchrone observatoren binnen de Lustre-taal, wat zowel runtime- als statische verificatie van cyber-fysieke systemen mogelijk maakt terwijl ondersteuning wordt geboden voor willekeurige nesting van begrensde eigenschappen en een globaal onbegrensde buitenste operator voor online monitoring.

Oorspronkelijke auteurs: Logan Kenwright, Partha Roop, Sobhan Chatterjee, Nathan Allen

Gepubliceerd 2026-08-14

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Logan Kenwright, Partha Roop, Sobhan Chatterjee, Nathan Allen

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een robot bouwt die een auto bestuurt, of een drone die pakketjes bezorgt. Deze machines leven in een wereld van continue beweging, maar hun hersenen zijn digitale computers die denken in kleine, discrete stappen, zoals frames in een film. Om ze veilig te houden, schrijven ingenieurs regels: "Kom nooit dichter dan 6 meter bij de auto voor je," of "Als je een hobbel raakt, moet je binnen 4 seconden weer op koers zijn." Het controleren of deze regels worden nageleefd is lastig. Je kunt niet naar de hele toekomst tegelijk kijken, want de robot weet niet wat er gaat komen. Je moet het stap voor stap volgen, zoals een scheidsrechter die pas fluit als een overtreding zeker is, en niet wanneer het slechts een 'misschien' is.

Hier komt een vakgebied genaamd "Runtime Verification" (runtime-verificatie) om de hoek kijken. Het is als een uiterst waakzame co-piloot die elke beweging van de robot in realtime volgt. De regels worden vaak geschreven in een speciale taal genaamd Signal Temporal Logic (STL), die erg goed is in het beschrijven van tijdgebonden regels. Maar er is een addertje onder het gras: de meeste tools die deze regels controleren, zijn als aparte auditors die achteraf naar een opname kijken, of ze gebruiken een andere taal dan de hersenen van de robot. Dit creëert een kloof. Als de auditor een andere taal spreekt, kun je er niet 100% zeker van zijn dat de robot de regels daadwerkelijk volgt terwijl hij rijdt. Je hebt een co-piloot nodig die exact dezelfde taal spreekt als de bestuurder, exact hetzelfde tempo denkt als de bestuurder, en op het juiste moment kan zeggen: "Ik weet zeker dat het veilig is," "Ik weet zeker dat het een crash is," of "Ik wacht nog even af om te zien."

Dit artikel introduceert een slimme nieuwe manier om die perfecte co-piloot te bouwen. De auteurs, werkend met een taal genaamd Lustre (een standaardtool voor het bouwen van veiligheidskritische software), hebben een techniek ontwikkeld om complexe, geneste tijdsregels direct om te zetten in code die meedraait met de robot. Denk aan het vertalen van een ingewikkelde set instructies naar een native app die in de hersenen van de robot leeft.

De grote doorbraak hier is het afhandelen van "geneste" regels. Stel je een regel voor die zegt: "Op elk moment in de komende 10 seconden moet je in staat zijn om binnen de volgende 4 seconden een veilige plek te vinden." Dit is een regel binnen een regel. Eerdere tools hadden moeite met deze complexiteit of konden ze niet in realtime uitvoeren. De methode van de auteurs breekt deze complexe regels af in een team van kleine, eenvoudige wachters (genaamd "leaves") die samenwerken. Elke wachter heeft een specifieke taak: hij houdt een specifiek evenement in de gaten binnen een specifieke tijdvenster. Als het evenement plaatsvindt, roept hij "Ja!"; als het venster sluit en het is niet gebeurd, roept hij "Nee!"; en als hij nog aan het wachten is, zegt hij "Onbekend."

Wat dit bijzonder maakt, is hoe ze omgaan met de "Onbekend"-status. In plaats van vast te lopen of te gokken, gebruikt het systeem een "driewaardige" logica. Het weet precies wanneer het genoeg informatie heeft om een definitieve beslissing te nemen. Bijvoorbeeld, als een regel vereist dat een veilige afstand gedurende 5 seconden wordt gehandhaafd, hoeft het systeem niet te wachten tot de volledige 5 seconden voorbij zijn om te weten of een overtreding onmogelijk is. Als de auto in seconde 2 crasht, weet het systeem dit onmiddellijk als een "Nee". Als de auto 3 seconden veilig blijft maar het venster nog open staat, zegt het systeem "Onbekend" totdat het venster sluit. Dit stelt het systeem in staat om eerder een definitief antwoord te geven dan de totale tijdlimiet van de regel zou afdwingen, wat een enorme winst is voor de veiligheid.

De auteurs hebben dit getest in twee scenario's: een stuiterend veer-massa-systeem (zoals een autoveringering) en een zelfrijdende auto die een auto volgt die plotseling remt. Ze lieten zien dat hun systeem veiligheidschendingen in realtime kan detecteren, waarbij het vaak de uitkomst al enkele "ticks" (tijdstappen) vóór de deadline van de regel bepaalt. Ze hebben ook een leuke, interactieve visualizer gebouwd waarmee je deze geneste regels op een scherm kunt volgen, waarbij precies wordt getoond welk deel van de regel werd voldaan en wanneer.

Cruciaal is dat omdat deze "co-piloot" in exact dezelfde taal is geschreven als de robot, deze gecontroleerd kan worden door een model checker (een tool die wiskundig bewijst dat software foutloos is) voordat de robot ooit de fabriek verlaat. Dit betekent dat hetzelfde stuk code twee meesters dient: het fungeert als een live veiligheidsmonitor terwijl de robot draait, en het fungeert als een wiskundig bewijs van veiligheid voordat hij begint. De auteurs hebben bewezen dat hun methd sound en compleet is, wat betekent dat het nooit een overtreding mist en nooit een vals alarm geeft, mits de regels binnen de ontworpen "begrensde" (bounded) tijdlimieten blijven. Ze hebben zelfs aangetoond dat hoewel het systeem de oneindige toekomst niet kan voorspellen, het effectief kan waken over systemen die eeuwig blijven draaien door een slimme "shift register"-truc te gebruiken die oude wachters hergebruikt voor nieuwe momenten in de tijd.

Kortom, dit artikel overbrugt de kloof tussen complexe tijdslogica en de echte wereld. Het verandelt abstracte logica in een levend, ademend onderdeel van de machine, waardoor veiligere en betrouwbaardere cyber-fysieke systemen mogelijk worden die kunnen bewijzen dat ze veilig zijn terwijl ze daadwerkelijk aan het werk zijn.

Technische Samenvatting: Synchronous Observers Revisited voor Runtime Verificatie van Lustre met behulp van STL

Probleemstelling
Signal Temporal Logic (STL) is een standaard formalisme voor het specificeren van temporele veiligheidseigenschappen in cyber-fysische systemen (CPS), met name voor runtime verificatie. De huidige STL-tools werken echter doorgaans op vooraf opgenomen of gesimuleerde signalen, of op abstracte automaatmodellen, in plaats van op de daadwerkelijk ingezette uitvoerbare code. Hierdoor ontbreeft een uitvoerbare, runtime-equivalentie semantiek voor geneste STL-eigenschappen die in lock-step draait met het gemonitorde systeem. Bovendien is het potentieel van deze observers voor runtime verificatie, terwijl synchrone talen zoals Lustre "synchronous observers" gebruiken voor statische verificatie, nog onvoldoende onderzocht. Een specifieke uitdaging ligt in het omgaan met de "driewaardige" aard van online monitoring: omdat gebonden temporele operatoren in de toekomst kijken, kan een monitor niet altijd direct bij een tick een definitief oordeel vellen, wat leidt tot een vertraging voordat een definitief verdict wordt bereikt.

Methodologie
De auteurs stellen een techniek voor om het synchrone fragment van STL (SSTL) direct te compileren naar synchrone observers binnen de datastroomtaal Lustre. De kern van de methodologie bestaat uit het "uitrollen" (unrolling) van geneste formules naar een eindige collectie niet-geneste verplichtingen, die elk een vast venster van discrete tijdstappen monitoren.

Driewaardige Streaming Semantiek: De aanpak hanteert een Kleene driewaardige semantiek (def_true, def_false, unknown). Bij elke tick geeft de observer een verdict uit op basis van het tot nu toe geobserveerde prefix. Unknown geeft aan dat de horizon van de formule nog niet is verstreken. Dit wordt geïmplementeerd met een paar Booleaanse signalen (pos, neg) die respectievelijk definitieve waarheid en definitieve onwaarheid vertegenwoordigen.
Primitieve Constructie (until_leaf): De auteurs synthetiseren een enkele herbruikbare Lustre-node, until_leaf, die de gebonden "until"-operator ( $U_{[a,b]}$ ) implementeert. Deze primitief houdt een precondition (het "alive"-signaal) en een postcondition (het "found"-signaal) bij over een specifiek venster. Het geeft def_true uit bij het vinden van een getuige (witness) en def_false bij vroege terminatie (falen van de precondition) of het verstrijken van het venster.
Recursieve Synthese: Geneste formules worden bottom-up gesynthetiseerd. Het systeem instantieert kopieën van de until_leaf-primitief voor elke vereiste start-tick van de buitenste operatoren. Deze kopieën worden aan elkaar gekoppeld met behulp van Kleene-logica regels voor conjunctie, disjunctie en negatie.
- Voor gebonden operatoren ( $\square_{[a,b]}$ , $\diamond_{[a,b]}$ ) synthetiseert de constructie de formule uit in een set bladeren (leaves) die overeenkomen met elke start-offset binnen het interval.
- Voor de ongebonden Globally-operator ( $\square$ ), die gebruikelijk is in vrij draaiende systemen, introduceren de auteurs een shift-register constructie. In plaats van oneindige observers te instantiëren, hergebruikt een register van grootte $H+1$ (waarbij $H$ de innerlijke horizon is) de staat, waardoor de monitor de "alive"-kopieën van de innerlijke formule onbeperkt kan volgen.
Visualisatie: Er is een interactieve, browser-gebaseerde tool geleverd om de driewaardige verdicts van geneste observers weer te geven over bewerkbare traces, wat helpt bij het debuggen en het intuïtief begrijpen van complexe, geneste temporele gedragingen.

Belangrijkste Bijdragen

Uitvoerbare Online Monitoring: De techniek synthetiseert observers die samen met het systeem in dezelfde synchrone taal (Lustre) worden gecompileerd, waardoor ze in lock-step draaien met de werkelijke uitvoerbare code in plaats van op gesimuleerde data.
Willekeurige Nesting met Modulaire Compilatie: In tegenstelling tot eerder werk (bijv. Bellanger et al.), dat beperkt was tot niet-geneste operatoren, ondersteunt deze methode willekeurige nesting van gebonden SSTL-eigenschappen.
Ongebonden Buitenste Operator: De aanpak staat een globaal ongebonden buitenste operator ( $\square$ ) toe die geschikt is voor het monitoren van vrij draaiende systemen, terwijl de innerlijke structuur gebonden blijft.
Dubbel Nut: De resulterende observers dienen een dubbel doel: ze fungeren als runtime monitors en dienen tevens als statische verificatieverplichtingen voor de Kind2 model checker zonder dat er een apart model nodig is.
Driewaardige Semantiek voor Runtime: De implementatie biedt causale Kleene-verdicts, waardoor monitors zich zo vroeg mogelijk aan een definitief oordeel kunnen committeren, vaak nog voordat de volledige horizon van de formule is verstreken.

Resultaten en Evaluatie
De auteurs hebben de techniek geëvalueerd aan de hand van twee casestudies: een veer-massa systeem en een scenario van een auto volgend adaptief cruise control (ACC) systeem met noodbraking.

Correctheid: Alle gesynthetiseerde observers zijn geverifieerd tegen de Kind2 model checker. Runtime- en statische verdicts kwamen bij elke eigenschap overeen (inclusclusief de mutual-exclusion invariant ( $pos \land neg = \text{false}$ )).
Prestaties: De observers werden gecompileerd naar C en uitgevoerd via de lv6 interpreter. De per-tick executiekosten werden gemeten in nanoseconden (variërend van ~6,7 ns tot ~206,5 ns afhankelijk van de complexiteit), wat ruim onder de typische milliseconde-schaal van regelperiodes ligt, wat de haalbaarheid voor online inzet bevestigt.
Vroege Terminatie: De driewaardige semantiek bleek effectief; in de casestudies bereikten gebonden eigenschappen definitieve verdicts strikt vóór hun theoretische horizonten. Bijvoorbeeld, een diep geneste eigenschap ( $P3$ ) bereikte een definitief oordeel 15 ticks eerder.
Ongebonden Gedrag: De ongebonden $\square$ operator fungeerde als een enkelvoudig falsificatiemechanisme, dat correct naar def_false verspringt wanneer overtredingen optreden (bijv. wanneer de afstand onder de veiligheidsdrempels zakt) en anders unknown blijft.

Significantie en Claims
Het artikel claimt de kloof te overbruggen tussen formele specificatie en uitvoerbare runtime monitoring voor synchrone CPS. Door observers direct in de taal van het systeem te synthetiseren, elimineren de auteurs de "modelleringskloof" die vaak voorkomt bij het verifiëren van abstracte modellen tegen ingezette code. Het werk demonstreert dat complexe, geneste temporele eigenschappen online gemonitord kunnen worden met lage latentie en hoge betrouwbaarheid. De auteurs positioneren hun werk als een uitbreiding van Bellanger et al. [5], waarbij specifiek de beperkingen met betrekking tot nestingdiepte en de oriëntatie naar enkel statische verificatie worden geadresseerd. De bijdrage wordt gepresenteerd als een systematische synthesetechniek die sound en compleet is met betrekking tot de expliciete driewaardige semantiek, gevalideerd door zowel runtime executie als statische model checking.

Beperkingen
De auteurs erkennen drie primaire beperkingen:

State Explosion: Het aantal bladeren is het product van de vensterbreedtes, wat kan leiden tot een exponentiële groei van de omvang van de observer bij grote intervallen (bijv. $\diamond_{[0,100]}$ ).
Closed-System Assumption: De casestudies modelleerden de plant binnen Lustre als een gesloten systeem. Het monitoren van echte open systemen met externe sensoring-inputs blijft een toekomstige stap.
Discreet Domein: De huidige aanpak opereert strikt binnen het gesamplede, gediscretiseerde domein en ondersteunt nog geen continue STL-robustness semantiek.

Meer zoals dit