🤖 AI

Runtime Enforcement of Hybrid System Properties

Dit artikel stelt een framework voor runtime-handhaving voor hybride systemen voor, dat hybride automaten en online bereikbaarheidsanalyse gebruikt om corrigerende acties te synthetiseren—zoals gebeurtenisonderdrukking, vertraging of invoeging—om veiligheidstoepassing te garanderen in real-time reactieve systemen zoals Adaptive Cruise Control met minimale computationele overhead.

Oorspronkelijke auteurs: Mir Md Sajid Sarwar, Srinivas Pinisetty, Rajarshi Ray, Thierry Jéron

Gepubliceerd 2026-06-11

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Mir Md Sajid Sarwar, Srinivas Pinisetty, Rajarshi Ray, Thierry Jéron

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 in een hypermoderne auto rijdt met een zeer slimme, maar soms roekeloze autopilot. Deze autopilot (de "controller") vertelt de auto voortdurend om op te trekken, af te remmen of op kruissnelheid te rijden. Echter, de autopilot weet niet altijd de exacte afstand tot de auto voor hem, of hij maakt een fout waardoor er een botsing ontstaat.

Dit artikel introduceert een veiligheidsbewaker die tussen de roekeloze autopilot en de weg in zit. Zijn taak is niet alleen om toe te kijken en te zeggen: "O nee, ik heb een botsing gezien!" (dat is slechts een camera die een crash registreert). In plaats daarvan grijpt deze bewaker actief in om de botsing te voorkomen voordat deze plaatsvindt.

Hieronder wordt uitgelegd hoe deze bewaker werkt, met behulp van eenvoudige analogieën:

1. Het Probleel: De "Stop-en-Go" Bewaker versus de "Vloeiende Stroom" Bewaker

De meeste bestaande veiligheidssystemen werken als een stop-en-go verkeerslicht. Ze controleren de snelheid en afstand van de auto alleen op specifieke, vaste momenten (zoals elke seconde). Als de auto om 1:00 uur veilig is en om 2:00 uur ook, gaan ze ervan uit dat de auto de hele tijd veilig was.

Maar auto's bewegen continu. Tussen 1:00 en 2:00 uur kan de auto naar voren zijn geracet en de auto voor hem hebben geraakt, om daarna weer af te remmen. Een "stop-en-go" bewaker mist dit.

Dit artikel stelt een nieuw soort bewaker voor dat werkt als een vloeiende rivier. Deze controleert niet alleen op de tikken van de klok; hij houdt de beweging van de auto continu in de gaten tussen de tikken door. Hij begrijpt dat de auto een "hybride" systeem is: het heeft digitale commando's (zoals "rem indrukken") en de fysieke realiteit (snelheid, afstand en acceleratie die allemaal tegelijkertijd plaatsvinden).

2. Het Instrument: De "Hybrid Automaton" Kaart

Om dit te doen, gebruikt de auteur een wiskundige kaart genaamd een Hybrid Automaton.

Denk aan deze kaart als een regelboek voor een videogame.
De game heeft verschillende "modi" (zoals Accelereren, Cruisen of Remmen).
De kaart heeft strikte regels voor elke modus. Bijvoorbeeld: in de modus Accelereren mag je alleen snel rijden als je ver genoeg van de auto voor je vandaan bent.
Als de auto te dichtbij komt, zegt de kaart: "STOP! Je betreedt de 'Crash Zone' (de Sink)."

De bewaker gebruikt deze kaart om de toekomst te voorspellen. Hij vraagt zich af: "Als ik het commando van de autopilot nu laat gebeuren, glijden we dan van de kaart af in de Crash Zone?"

3. De Magische Trucs: Hoe de Bewaker Fouten Herstelt

Wanneer de bewaker ziet dat de autopilot op het punt staat een fout te maken, heeft hij drie magische instrumenten om dit direct te herstellen:

De Pauzeknop (Delay): De autopilot zegt: "Versnel!" op 1,0 seconde. De bewaker zegt: "Nog niet! Wacht tot 1,29 seconden, wanneer de auto voor je ver genoeg weg is." Hij houdt het commando vast in een buffer en geeft het op het perfecte moment vrij.
De Gum (Suppression): De autopilot zegt: "Versnel!" op 9,0 seconden, maar de auto is te dichtbij. De bewaker zegt: "Nee," en verwijdert dat commando simpelweg. Hij vervangt het door een "niets doen"-commando (een stutter genoemd), waardoor de auto veilig kan uitrollen.
De Ghost Driver (Insertion): Soms is de autopilot stil, maar drijft de auto richting gevaar. De bewaker wacht niet op een commando; hij voegt een nieuw commando in. Hij zegt: "Omdat je niets doet, zal ik de auto nu vertellen om te 'Cruisen' of te 'Remmen' om ons veilig te houden."

4. De Test in de Praktijk: Adaptieve Cruise Control

De auteurs hebben dit getest op een Cruise Control van een zelfrijdende auto.

Het Scenario: De hoofdcomputer van de auto was defect en bleef de auto vertellen om te accelereren, zelfs toen de auto gevaarlijk dicht bij de auto voor hem kwam.
Het Resultaat: Zonder de bewaker crashte de auto (de afstand daalde onder de 10 meter).
Met de Bewaker: De bewaker hield de snelheid en afstand continu in de gaten. Hij vertraagde enkele acceleratie-commando's, verwijderde andere en voegde rem-commando's in tussen de reguliere controles door. De auto bleef veilig en kwam nooit dichter dan 10 meter bij de auto voor hem.

5. Waarom het Belangrijk is

De auteurs beweren dat dit systeem ongelooflijk snel is. Het voegt bijna geen vertraging toe aan het denkproces van de auto (slechts ongeveer 4,67 milliseconden per controle). Dit betekent dat het in real-time gebruikt kan worden in echte auto's zonder ze te vertragen.

Samenvattend: Dit artikel bouwt een "slim veiligheidsnet" voor complexe machines zoals zelfrijdende auto's. In tegen tegenstelling tot oudere systemen die alleen de regels op vaste tijden controleren, houdt dit net de beweging van de machine continu in de gaten, waarbij het gevaar voorspelt en de commando's van de machine direct aanpast (het pauzeren, verwijderen of toevoegen van acties) om ervoor te zorgen dat de veiligheidsregels nooit worden overtreden.

Technische Samenvatting: Runtime Enforcement van Hybride Systeemeigenschappen

Probleemstelling

Autonome en cyber-fysieke systemen (CPS) opereren in onzekere, dynamische omgevingen waar traditionele ontwerp-tijd verificatie (formele verificatie, simulatie) vaak onvoldoende is om veiligheid te garanderen. Hoewel Runtime Verification (RV) schendingen van eigenschappen kan detecteren tijdens de uitvoering, is dit een passief proces dat geen schendingen voorkomt. Runtime Enforcement (RE) adresseert dit door actief in te grijpen om het systeemgedrag te wijzigen. Bestaande RE-frameworks kampen echter met aanzienlijke beperkingen wanneer ze worden toegepast op complexe reactieve systemen:

Discrete versus Continue Dynamiek: De meeste frameworks vertrouwen op ongetimede of discrete-time specificaties (bijv. Discrete Timed Automata). Deze zijn ontoereikend voor systemen die complexe continue dynamiek vertonen, omdat ze de evolutie in dense-time niet kunnen modelleren of kunnen ingrijpen tussen discrete bemonsteringspunten.
Interventie Granulariteit: Bestaande benaderingen zijn vaak beperkt tot het vertragen of onderdrukken van gebeurtenissen op discrete tijdstippen. Ze missen de capaciteit om gebeurtenissen op willekeurige tijdstippen in te voegen of om continue-time monitoring uit te voeren, wat crual is voor het handhaven van veiligheid in systemen met continue staatstrajecten.
Reactieve Systeembeperkingen: Veel handhavingsmechanismen (bijv. het stoppen van de uitvoering of langdurig bufferen) zijn onhaalbaar voor reactieve systemen die onmiddellijke respons vereisen om liveness te behouden en strikte timing-constraints te voldoen.

Het kernprobleem dat wordt geadresseerd is het gebrek aan een runtime enforcement framework dat in staat is om veiligheidseigenschappen gespecificeerd als Hybrid Automata (HA) te verwerken, wat continue-time monitoring en proactieve, fijnmazige corrigerende interventies (onderdrukking, vertraging en invoeging) mogelijk maakt voor reactieve systemen.

Methodologie

Het paper stelt een runtime enforcement framework voor waarbij veiligheidseisen worden gemodelleerd met behulp van Safety Hybrid Automata (HA). Dit formalisme legt zowel discrete executiestappen (via transitie-guards) als continue dynamiek (via differentiaalvergelijkingen en staat-invarianten) vast.

Kerncomponenten

Safety Hybrid Automaton (S): De eigenschap $\phi$ wordt geformaliseerd als een HA met een unieke niet-accepterende "Sink" (valstrik) locatie. Transities naar de Sink treden op wanneer een veiligheidsinvariant (bijv. minimale afstand) wordt geschonden. Alle andere locaties zijn accepterend.
Enforcer Function ( $E_\phi$ ): De enforcer fungeert als een laag tussen de System under Monitor (SuM) en de omgeving. Het ontvangt een stroom van input-events en omgevingsstatussen op discrete synchronisatiepunten (clock ticks, aangeduid als $ptick$).
Correctieve Acties: De enforcer synthetiseert een gecorrigeerde output-stroom door:
- Onderdrukken (Suppressing): Een onveilige event wegwerpen en een "stutter" event uitzenden om de vorige staat te behouden.
- Vertragen (Delaying): Een event uitstellen naar een later tijdstip wanneer de guard-conditie wordt voldaan.
- Invoegen (Inserting): Proactief een nieuwe event invoegen op een willekeurig tijdstip (zelfs tussen $pticks$) om een dreigende invariant-schending te voorkomen.
Online Algoritme: Het enforcement algoritme werkt in een synchrone reactieve loop:
- Initialisatie: De HA wordt geïnitialiseerd op basis van de huidige omgevingsstatus.
- Tijdverloop: Het algoritme simuleert de continue evolutie van de systeemstatus over het tijdsinterval tot de volgende event of $ptick$.
- Invariant Checking: Het verifieert of het continue traject binnen de huidige locatie's invariant blijft.
- Beslissingslogica:
  - Als de invariant standhoudt en de guard voor de inkomende event wordt voldaan, wordt de event doorgegeven.
  - Als de invariant standhoudt maar de guard niet wordt voldaan, wordt de event onderdrukt (vertraagd).
  - Als de invariant wordt geschonden, controleert het algoritme of er vertraagde acties mogelijk zijn. Indien deze niet bestaan, synthetiseert en voegt het een nieuwe actie in (uit de set van enabled transitions) om het systeem terug te sturen naar een veilige staat vóór de volgende $ptick$.

Formele Constraints

De enforcer is gedefinieerd om vier belangrijke constraints te voldoen:

Soundness (Correctheid): De output-sequentie moet altijd de veiligheidseigenschap $\phi$ voldoen.
Instantaneity (Onmiddellijkheid): De enforcer moet direct reageren op inputs en kan events proactief invoegen.
Monotonicity (Monotoniciteit): De output voor een uitgebreide input-sequentie moet een voortzetting zijn van de output voor het prefix.
Transparency (Transparantie): De enforcer grijpt minimaal in; als het systeemgedrag veilig is, fungeert de enforcer als een identiteitsfunctie.

Belangrijkste Bijdragen

Nieuw Framework: Een runtime enforcement framework voor reactieve CPS gebaseerd op Hybrid Automata specificaties, wat continue-time monitoring en corrigerende interventie mogelijk maakt.
Formele Definitie: Een formele definitie van het runtime enforcement probleem voor veiligheidseigenschappen gespecificeerd via Safety Hybrid Automata, waarmee RE wordt uitgebreid voorbij untimed en discrete-time formalismen.
Enforceability Conditions: De vaststelling van condities voor vervolgbaarheid (enforceability), waarbij vereist is dat vanuit elke niet-schendende staat een accepterende staat bereikbaar moet zijn via enabled transitions.
Online Algoritme: Een algoritme dat in staat is om veilige executie-traces te synthetiseren door middel van event-onderdrukking, vertraging en invoeging, terwijl de timing-constraints van het systeem worden gerespecteerd.
Casestudy: Een gedetailleerde toepassing op een Adaptive Cruise Control (ACC) systeem, waarbij de synthese van veilige traces uit potentieel defecte controller-outputs wordt gedemonstreerd.

Resultaten en Evaluatie

Het voorgestelde framework werd geëvalueerd met behulp van een Adaptive Cruise Control (ACC) scenario waarbij de primaire controller als defect werd aangenomen, waarbij deze potentieel commando's geeft die de minimale veilige afstand ( $d > 10$ meter) schenden.

Scenario: Het systeem monitorde variabelen zoals acceleratie ( $a$ ), snelheid ( $v$ ) en relatieve afstand ( $d$ ). De controller genereerde een sequentie van events (versnellen, cruisen, etc.) die zonder interventie tot een botsing (afstand $< 10$ m) zouden leiden.
Enforcement Uitkomst: De enforcer onderschepte de onveilige event-stroom succesvol. Het onderdrukte onveilige acceleratie-commando's, vertraagde andere en voegde deceleratie-commando's in op precieze tijdstippen (bijv. $t \approx 10.67$ ) om de veiligheidsinvariant te handhaven.
Prestaties:
- Latency (Latentie): De gemiddelde responstijd per event was 4.67 milliseconden.
- Overhead: Het framework introduceerde verwaarloosbare computationele overhead; het verwerkte de volledige trace in 15.098 seconden op standaard hardware (Intel Core i5, 8GB RAM).
- Conclusie: De resultaten bevestigen het vermogen van het framework om effectief te opereren in high-frequency reactieve omgevingen zonder de strikte timing-constraints te schenden.

Betekenis en Claims

Het paper claimt dat de primaire betekenis ligt in het overbruggen van de kloof tussen discrete-time enforcement en de continue aard van cyber-fysieke systemen. Door gebruik te maken van Hybrid Automata, stelt het framework:

Dense-time monitoring mogelijk tussen discrete bemonsteringspunten, een capaciteit die ontbreekt in Discrete Timed Automata (DTA) benaderingen.
Proactieve interventie (invoeging van events) mogelijk op willekeurige tijdstippen, in plaats van beperkt te zijn tot discrete ticks.
Fijnere controle over het systeemgedrag, wat zorgt voor continue naleving van veiligheidseisen in real-time.

De auteurs stellen dat, naar hun weten, geen enkel bestaand enforcement framework ondersteuning biedt voor expressieve HA specificaties die geschikt zijn voor reactieve systemen. Zij positioneren dit werk als een stap naar sterkere veiligheidsgaranties voor autonome systemen die opereren in onzekere omgevingen, waarbij zij verder gaan dan passieve verificatie naar actieve, continuous-time enforcement.

Het paper blijft bescheiden over de reikwijdte en erkent dat de huidige benadering beperkt is tot veiligheidseigenschappen (prefix-gesloten specificaties) en beslisbare subklassen van hybride automaten. Toekomstig werk wordt geïdentificeerd als noodzakelijk voor het afhandelen van liveness-eigenschappen, niet-lineaire dynamiek, stochastische onzekerheid en gedistribueerde multi-agent systemen.