Automated LTL Specification Generation from Industrial Aerospace Requirements

Titel: Geautomatiseerde generatie van LTL-specificaties vanuit industriële aerospace-vereisten

1. Het Probleem

In de ontwikkeling van veiligheidskritieke aerospace-software is Linear Temporal Logic (LTL) de standaard voor het specificeren van complexe systeemeigenschappen. Echter, er bestaat een aanzienlijke kloof tussen de praktijk en de theorie:

• Handmatige vertaling: Het vertalen van natuurlijke taal (NL) vereisten naar formele LTL-eigenschappen is arbeidsintensief, foutgevoelig en vereist zeldzame expertise in zowel aerospace-techniek als formele methoden.
• Beperkingen van bestaande tools: Bestaande NL-naar-LTL-tools (zoals NL2SPEC, NL2TL) presteren goed op synthetische benchmarks, maar falen vaak in industriële settings.
• Oorzaken van falen: Industriële aerospace-documenten bevatten:
  1. Heterogene context: Vereisten zijn niet geïsoleerde zinnen; hun betekenis is afhankelijk van interface-beschrijvingen (signalen, datatypen, initiële waarden) en roepvoorwaarden (bijv. controlecycli van 128 ms).
  2. Domeinspecifieke terminologie: Technische termen fungeren als placeholders voor complexe logica die zonder domeinkennis niet correct kan worden gemapt naar code-niveau variabelen.
  3. Impliciete temporele logica: Temporele operatoren (zoals "volgende stap" of Next) en logische relaties worden vaak niet expliciet vermeld in de tekst, maar zijn impliciet in de controlelogica.

Algemene Large Language Models (LLM's) lijden aan "contextuele blindheid" ten opzichte van engineering-artefacten en kunnen deze impliciete aannames niet correct modelleren, wat leidt tot semantisch onjuiste specificaties.

2. Methodologie: Het AeroReq2LTL Framework

Het paper introduceert AeroReq2LTL, een systeem dat LLM's combineert met twee industriële innovaties om de vertaling te automatiseren. De workflow bestaat uit drie fasen:

Fase 1: Dual-stream Context Reconstruction (Contextherstel)
In plaats van vereisten als losse zinnen te behandelen, extrahert het systeem twee informatiestromen uit het PDF-document:

• Doelstroom (Target Stream): Complete functionele paragrafen met vereisten, inclusief roepvoorwaarden.
• Kennisstroom (Knowledge Stream): Technische metadata uit interface-beschrijvingstabellen (signaannamen, datatypen, bereik).

Fase 2: NL-naar-TNL Rewriting (Semantische herschrijving)
De natuurlijke taal wordt omgezet in Templated Natural Language (TNL). Dit gebeurt via twee kerncomponenten:

• SpaceKG (Domain Grounding): Een domeinspecifieke datadictionary die automatisch engineering-artefacten (zoals interface-tabellen) inleest. Het normaliseert complexe technische jargon naar precieze, code-niveau atomaire proposities (bijv. het vertalen van "helling < 0.15°/s" naar de variabele dwCount).
• SpaceRDL (Structured Requirement Description Language): Een gestructureerde template-taal die LLM's dwingt om impliciete temporele en logische relaties expliciet te maken. Het forceert vereisten in vaste velden zoals workmode, condition, timing en action.

Fase 3: TNL-naar-LTL Converting (Deterministische synthese)
Omdat de TNL-uitvoer gestructureerd en semantisch gebaseerd is, wordt de probabilistische generatie van LLM's vervangen door deterministische vertaalregels. Dit garandeert dat de uiteindelijke LTL-specificaties syntactisch geldig zijn en wiskundig overeenkomen met de bedoelde controlelogica.

3. Belangrijkste Bijdragen

1. AeroReq2LTL Framework: Een end-to-end oplossing die de kloof tussen industriële vereisten en formele specificaties overbrugt door context en domeinkennis te integreren.
2. SpaceKG: Een dynamische kennisbasis die technische termen koppelt aan concrete systeemvariabelen, waardoor "grounding errors" (zoals het verwarren van variabelen) worden voorkomen.
3. SpaceRDL & TNL: Een template-systeem dat impliciete temporele logica (zoals controlecycli en modewisselingen) expliciet maakt voordat de vertaling naar LTL plaatsvindt.
4. Industriële Validatie: Het systeem is getest op echte aerospace-productievereisten en is direct integreerbaar met bestaande verificatietools (zoals TRACE).

4. Resultaten

Het systeem is geëvalueerd op een dataset van 79 productievereisten uit het Sun Search Control Software (SSCS)-systeem voor lage-aarde-orbit satellieten. De resultaten werden vergeleken met baselines (SimPro, NL2LTL, NL2SPEC) en verschillende LLM-achtergronden (GPT-4o, GPT-3.5, DeepSeek).

• Prestaties van AeroReq2LTL:
  • Precisie: 85%
  • Recall: 88%
  • Dit is een aanzienlijke verbetering ten opzichte van de beste baseline (NL2SPEC + GPT-4o), die slechts 61% precisie en 61% recall haalde.
• Ablatiestudies:
  • Zonder SpaceKG daalde de precisie naar 69% (veel fouten door verkeerde variabele-mapping).
  • Zonder SpaceRDL daalde de precisie naar 52% (fouten door het missen van temporele operatoren en logische structuur).
• Verificatie: De gegenereerde LTL-specificaties konden direct worden ingevoerd in de industriële verificatietool TRACE. Van de 67 correct vertaalde vereisten werden er 63 succesvol geverifieerd over diverse functionele modules.

5. Betekenis en Impact

• Oplossing voor de "Formalisatie-flesnek": Het paper toont aan dat de hoge kosten en risico's van handmatige formalisatie in de aerospace-industrie kunnen worden verminderd door domein-specifieke kennis te integreren in LLM-workflows.
• Van "Black Box" naar Ingenieursproces: Door de vertaling op te splitsen in een gestructureerde tussenstap (TNL) en deterministische regels, wordt het proces controleerbaar en reproduceerbaar, in plaats van afhankelijk van de "gok" van een generatieve AI.
• Schaalbaarheid: Hoewel de huidige evaluatie zich richtte op één module, biedt het framework een pad naar schaalbare, geautomatiseerde softwareverificatie voor grotere, veiligheidskritieke systemen (zoals auto's en medische apparatuur) die vergelijkbare documentatiestandaarden hanteren.

Kortom, AeroReq2LTL bewijst dat geautomatiseerde formele specificatie in de praktijk haalbaar is, mits de specifieke complexiteit van industriële documentatie (context, terminologie en impliciete logica) systematisch wordt aangepakt.