💻 computer science

Separation Logic for Verifying Physical Collisions of CNC Programs

Dieser Beitrag stellt einen Formalen Verifikationsrahmen vor, der den CNC-Arbeitsraum als einen räumlichen Heap modelliert und Separation Logic anwendet, um physische Kollisionen als logische Datenrennen zu erkennen, wodurch die Abhängigkeit von iterativen Simulationen für eine sicherere, autonome Fertigung verringert wird.

Ursprüngliche Autoren: Yeonseok Lee

Veröffentlicht 2026-05-21

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Yeonseok Lee

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie betreiben eine hochgeschwindigkeitsfähige, automatisierte Fabrik, in der ein Roboterarm (die CNC-Maschine) ein Metallstück bearbeitet. Traditionell führen Ingenieure Tausende von Computersimulationen durch, um sicherzustellen, dass der Roboter nicht seinen eigenen Arm gegen das Metall oder den Tisch schleudert. Sie beobachten die Bewegung des Roboters in einer virtuellen Welt in der Hoffnung, einen Zusammenstoß zu erkennen, bevor er in der Realität stattfindet. Doch wenn Sie das Design auch nur geringfügig ändern, müssen Sie all diese Simulationen erneut durchführen. Es ist langsam, repetitiv und bietet keine 100-prozentige Garantie.

Dieser Artikel schlägt eine völlig andere Denkweise für die Sicherheit vor. Anstatt einen Film der Roboterbewegung zu beobachten, behandelt er den Fabrikboden wie den Speicher eines Computers.

Hier ist die einfache Aufschlüsselung ihrer Idee:

1. Der Fabrikboden ist ein „Speichergitter"

Stellen Sie sich den gesamten Arbeitsraum der Maschine als ein riesiges 3D-Gitter aus winzigen Würfeln vor (wie Pixel, aber in 3D).

Der alte Weg: Sie berechnen die exakte Kurve des Roboterarms, während er sich durch die Luft bewegt. Dies ist mathematisch unübersichtlich und schwer zu beweisen, dass es sicher ist.
Der neue Weg: Die Autoren sagen: „Lassen Sie uns aufhören, uns um die glatten Kurven zu sorgen. Sehen wir uns einfach an, welche Würfel belegt sind."
- Wenn ein Würfel das Werkzeug enthält, ist er als „Werkzeug" markiert.
- Wenn ein Würfel den Metallblock enthält, ist er als „Rohling" markiert.
- Wenn ein Würfel eine Spannvorrichtung enthält, ist er als „Umgebung" markiert.
- Wenn ein Würfel leer ist, ist er als „Leer" markiert.

2. Der „Parser-Prover-Handshake" (Der Übersetzer)

Die Maschine spricht eine Sprache aus glatten, Gleitkommazahlen (wie X = 10,5432). Der Sicherheitsprüfer spricht eine Sprache aus strengen, ganzen Zahlen (wie „Würfel 10", „Würfel 11").

Der Artikel stellt einen Übersetzer (genannt Parser) vor, der zwischen dem Maschinencode und dem Sicherheitsprüfer sitzt.

Die Aufgabe: Der Übersetzer nimmt den glatten, wellenförmigen Pfad, den der Roboter möglicherweise nimmt, und rastet ihn in die nächstgelegenen Gitterwürfel ein. Er fügt auch einen kleinen „Sicherheitspuffer" hinzu (wie das Anlegen eines flauschigen Mantels um das Werkzeug), um sicherzustellen, dass der Roboter, selbst wenn er minimal wackelt, nichts trifft.
Das Ergebnis: Bis der Sicherheitsprüfer das Problem sieht, gibt es keine wellenförmigen Linien oder Dezimalstellen mehr. Es ist nur eine Liste spezifischer Würfel: „Das Werkzeug ist hier, das Metall ist dort, und der Weg ist frei."

3. Kollisionen sind „Datenrennen"

In der Computerprogrammierung tritt ein „Datenrennen" auf, wenn zwei Programme versuchen, gleichzeitig denselben Speicherort zu beschreiben, was zu einem Absturz führt.

Die große Idee des Artikels: Ein physischer Zusammenstoß in einer Fabrik ist genau dasselbe. Wenn das „Werkzeug" versucht, das Eigentum an einem Würfel zu beanspruchen, der bereits dem „Spannwerkzeug" gehört, ist dies ein räumliches Datenrennen.
Die Logik: Die Autoren verwenden ein spezielles mathematisches System namens Separation Logic. Dieses System hat eine einfache Regel: Zwei Dinge können nicht gleichzeitig dasselbe Stück Raum besitzen.
Die Prüfung: Der Sicherheitsprüfer (der Prover) betrachtet die Liste der Würfel. Er fragt: „Überlappen sich die Würfelliste des Werkzeugs mit der Liste des Spannwerkzeugs?"
- Wenn die Antwort Nein lautet, ist der Zug sicher.
- Wenn die Antwort Ja lautet, sagt die Mathematik sofort „FALSCH". Das System stoppt die Maschine sofort, beweist, dass ein Zusammenstoß passieren würde, ohne jemals eine langsame Simulation durchführen zu müssen.

4. Metall schneiden ist „Speicher löschen"

Wenn der Roboter das Metall schneidet, entfernt er Material.

In diesem neuen System ist das Schneiden nicht nur eine visuelle Änderung, sondern eine logische Aktualisierung.
Während sich das Werkzeug durch die Metallwürfel bewegt, ändert das System diese Würfel logisch von „Rohling" zu „Leer".
Es ist wie beim Spielen von Tetris, wo die Quadrate, die der fallende Block berührt, vom Brett verschwinden. Die Mathematik beweist, dass das Werkzeug nur Quadrate berührt, die tatsächlich „Rohling" und nicht „Spannwerkzeug" waren.

5. Zusammenarbeiten (Parallelität)

Was ist, wenn zwei Roboter am selben Tisch arbeiten?

Der Artikel verwendet eine Erweiterung ihrer Logik, um dies zu handhaben. Er behandelt den Arbeitsraum wie ein gemeinsames Büro.
Wenn Roboter A einen bestimmten Bereich (eine „Übergabezone") nutzen muss, um ein Teil an Roboter B weiterzugeben, fungiert das System wie eine Sperre.
Roboter A „sichert" die Zone (beansprucht das Eigentum an diesen Würfeln). Roboter B kann diese Zone nicht betreten, bis Roboter A fertig ist und sie „entsperrt" (gibt die Würfel als „Leer" zurück).
Dies verhindert, dass die beiden Roboter gegeneinander kollidieren, da die Mathematik beweist, dass sie niemals gleichzeitig dieselbe „Sperre" halten können.

6. Drehende Tische (5-Achsen-Maschinen)

Einige Maschinen haben Tische, die sich drehen, während sich das Werkzeug bewegt. Dies ist normalerweise sehr schwer zu berechnen.

Der Trick des Artikels: Der Übersetzer (Parser) führt die gesamte schwere Drehmathematik durch, bevor der Sicherheitsprüfer sie betrachtet.
Er berechnet genau, welche Würfel der sich drehende Metallblock durchstreifen wird, und wandelt dies in eine einfache Liste von „Belegten Würfeln" um.
Der Sicherheitsprüfer prüft dann nur, ob sich die Liste des Werkzeugs und die Liste des sich drehenden Metalls überschneiden. Wenn sie es nicht tun, ist der Zug sicher.

Zusammenfassung

Anstatt zu versuchen, die Physik eines abstürzenden Roboters zu simulieren, verwandelt dieser Artikel den Fabrikboden in ein logisches Rätsel.

Übersetzen Sie den glatten Pfad des Roboters in ein Gitter aus Würfeln.
Prüfen Sie, ob sich die Würfel des Werkzeugs mit denen des Spannwerkzeugs oder des Metalls überschneiden.
Beweisen Sie die Sicherheit, indem Sie zeigen, dass sie vollständig getrennt (disjunkt) sind.

Wenn die Mathematik sagt, dass sich die Würfel nicht überschneiden, ist die Maschine garantiert sicher. Wenn sie sich überschneiden, beweist die Mathematik, dass ein Zusammenstoß unvermeidlich ist, und stoppt die Maschine, bevor sie überhaupt beginnt. Dies ersetzt Tausende von langsamen, repetitiven Tests durch einen einzigen, sofortigen mathematischen Beweis.

Technische Zusammenfassung: Separationslogik zur Verifikation physischer Kollisionen von CNC-Programmen

1. Problemstellung

Die traditionelle Sicherheitsverifikation für die computergesteuerte Fertigung (CNC) stützt sich stark auf geometrische Simulationen und Analyse von überstrichenen Volumina. Obwohl diese Methoden effektiv sind, um offensichtliche G-Code-Fehler zu identifizieren, leiden sie unter fundamentalen Einschränkungen:

Fehlender symbolischer Beweis: Sie bieten probabilistisches Vertrauen anstelle von deterministischen, symbolischen Sicherheitsbeweisen.
Rechenkosten: Sie erfordern wiederholte Testzyklen, insbesondere wenn Spezifikationen oder G-Code geändert werden.
Umgang mit Unsicherheit: Sie haben Schwierigkeiten, kontinuierliche kinematische Variablen, nicht-deterministische Schnellpositionierungspfade und mechanische Variabilitäten (z. B. Servo-Verzögerung) rigoros zu berücksichtigen, ohne rechnerisch extrem aufwendig zu werden.
Skalierbarkeit: Bestehende Methoden versagen häufig bei der effizienten Skalierung auf komplexe Mehrachsen-Umgebungen (z. B. 5-Achsen-Tisch-Tisch-Konfigurationen) und kollaborative Mehrwerkzeug-Systeme.

Die Arbeit geht davon aus, dass physische Kollisionen in der CNC-Bearbeitung als logische Widersprüche innerhalb eines verwalteten Ressourcenmodells neu definiert werden können, wodurch eine deterministische Alternative zur stochastischen Simulation geboten wird.

2. Methodik

Der vorgeschlagene Rahmen führt eine Parser-Prover-Handshake-Architektur ein, die kontinuierliche physikalische Kinematik von diskreter formaler Logik entkoppelt. Dieser Ansatz konzeptualisiert den physikalischen CNC-Arbeitsraum als räumlichen Heap und behandelt physische Belegung als verwaltete logische Ressource.

2.1 Architektonische Entkopplung

Das System operiert durch eine strikte Grenze zwischen zwei Domänen:

Der Parser (Kontinuierliche Domäne): Agiert als virtuelle Maschine, die rohen G-Code, Werkzeuggeometrie und Sicherheitsabstände konsumiert. Er führt kontinuierliche kinematische Variablen (Gleitkommakoordinaten, Vorschubgeschwindigkeiten) und physikalische Unsicherheiten in eine diskrete Ganzzahldomäne ( $Z^3$ ) über. Er nutzt Minkowski-Summen, um Werkzeugvolumen um einen benutzerdefinierten Sicherheitsabstand ( $\epsilon$ ) zu erweitern, und setzt den 3D-Bresenham-Algorithmus ein, um diskrete Voxel-Pfade für lineare Interpolation (G01) und Begrenzungsboxen für Schnellpositionierung (G00) zu generieren.
Der SL-Prover (Diskrete Domäne): Operiert strikt auf den vom Parser emittierten diskreten räumlichen Mengen. Er fungiert als Speicherverwalter und bewertet Separationslogik (SL)-Tripel gegen einen räumlichen Heap ( $h$ ). Der Prover fragt keinen Variablenpeicher ab; er validiert ausschließlich räumliche Disjunktheit.

2.2 Das räumliche Heap-Modell

Der physikalische Arbeitsraum wird auf eine endliche partielle Funktion $h: Z^3 \rightharpoonup \{Tool, Environment, Stock, Empty\}$ abgebildet.

Räumliche Datenrennen: Physische Kollisionen werden als „Räumliche Datenrennen" neu definiert, die auftreten, wenn zwei verschiedene physische Ressourcen (z. B. Werkzeug und Umgebung) versuchen, gleichzeitig denselben diskreten Speicheradressen zu beanspruchen.
Trennende Konjunktion ( $*$ ): Der zentrale logische Operator besagt, dass Teilformeln für disjunkte Speicherbereiche gelten. Wenn $R(C_1, \theta_1) * R(C_2, \theta_2)$ ausgewertet wird, ist dies nur erfüllbar, wenn $C_1 \cap C_2 = \emptyset$ . Ein nicht-leerer Schnitt macht die Logik unerfüllbar und signalisiert deterministisch einen Fehler.

2.3 Verifikationspipeline

Der Verifikationsprozess folgt einer unidirektionalen Pipeline:

Eingabe: Roher G-Code, Werkzeugmaskengeometrie, Sicherheitsabstand ( $\epsilon$ ) und Auflösungsfaktor.
Diskretisierung: Der Parser wandelt Eingaben in diskrete räumliche Mengen ( $V_{start}, V_{final}, V_{path}$ ) um.
Logische Inferenz: Der Prover bewertet das Separationslogik-Tripel $\{ \Sigma_0 \} \text{CSL} \{ \Sigma_{final} \}$ ${Σ_{0}} CSL {Σ_{f ina l}}$ .
- Vorbedingung ( $\Sigma_0$ ): Behauptet die anfängliche disjunkte Eigentümerschaft von Werkzeug, Umgebung, Rohling und leerem Raum.
- Befehl (CSL): Repräsentiert die diskrete Bewegung (z. B. G00, G01) als Heap-Mutationen.
- Nachbedingung ( $\Sigma_{final}$ ): Behauptet das aktualisierte Eigentum nach der Verschiebung des Werkzeugs und dem Materialabtrag.

2.4 Erweiterungen für Parallelität und Mehrachsen

Concurrent Separation Logic (CSL): Für Mehrwerkzeug- oder kollaborative Umgebungen wird der räumliche Heap in threadlokale Teil-Heaps ( $h_{local}$ ) und einen geteilten Heap ( $h_{shared}$ ) partitioniert. Physische Übergabe werden als formale Eigentumsübertragungen mittels kritischer Regionen (with Res do C) verifiziert, was gegenseitigen Ausschluss ohne dynamische Sperren gewährleistet.
Mehrachsen-Kinematik: Der Rahmen skaliert auf 5-Achsen-Betrieb, indem das Schneidwerkzeug und das drehbare Werkstück als zwei parallele, sich gegenseitig verändernde räumliche Threads behandelt werden. Der Parser berechnet vorab das rotatorische überstrichene Volumen des Rohlings (unter Verwendung von Rotationsmatrizen) und das lineare überstrichene Volumen des Werkzeugs und präsentiert beide als diskrete Mengen dem Prover. Dies abstrahiert komplexe trigonometrische Kinematik von der Beweisengine.

3. Hauptbeiträge

Formale Neudefinition von Kollisionen: Die Arbeit stellt eine formale Korrespondenz zwischen physischer Belegung und logischem Speichereigentum her und definiert physische Kollisionen als logische „Räumliche Datenrennen".
Parser-Prover-Handshake: Eine neuartige architektonische Grenze, die kontinuierliche Unsicherheiten in eine diskrete Ganzzahldomäne überführt, wodurch der Prover innerhalb eines handhabbaren Fragments der Separationslogik operieren kann, ohne die Komplexität allgemeiner Zeigerarithmetik zu bewältigen.
Integration geometrischer Sicherheitsabstände: Die Methodik integriert Minkowski-Summen, um formale Sicherheitsabstände ( $\epsilon$ ) direkt innerhalb der diskreten Logik bereitzustellen und reale mechanische Unsicherheiten zu berücksichtigen.
Skalierbarkeit auf fortschrittliche Kinematik: Der Rahmen unterstützt nativ Mehrachsen- (z. B. 5-Achsen) und parallele Mehrwerkzeug-Umgebungen, indem das Werkstück als dynamisch veränderbare räumliche Ressource modelliert und Concurrent Separation Logic zur Verifikation geteilter Arbeitsräume genutzt wird.

4. Ergebnisse und Validierung

Die Arbeit demonstriert die Methodik durch:

Deterministische Verifikation: Das System verifiziert erfolgreich sichere Trajektorien, indem es die Erfüllbarkeit von Separationslogik-Tripeln beweist.
Kollisionserkennung: In einer Fallstudie, die eine Schnellfahrt in eine Vorrichtung beinhaltet, erkennt das System ein „Räumliches Datenrennen" (nicht-leerer Schnitt beanspruchten Speichers) und wechselt deterministisch vor der physischen Ausführung in einen Fehlerzustand.
Parallelität und Übergabe: Der Rahmen validiert die parallele Ausführung von zwei Werkzeugen in disjunkten Räumen und die sichere sequenzielle Übergabe einer geteilten Ressource und beweist, dass die trennende Konjunktion gegenseitigen Ausschluss erzwingt.
Mehrachsen-Verifikation: Der Ansatz verifiziert erfolgreich 5-Achsen-Betrieb, indem er komplexe rotatorische Kinematik auf diskrete Voxel-Mengen reduziert und beweist, dass die Pfade von Werkzeug und Rohling weder die Umgebung noch einander schneiden.

5. Bedeutung und Behauptungen

Die Arbeit behauptet, dass dieser Ansatz eine deterministische Alternative zur traditionellen geometrischen Simulation bietet und symbolische Sicherheitsbeweise anstelle von probabilistischem Vertrauen liefert. Als Ergänzung zur Simulation zielt der Rahmen darauf ab:

Iteratives Testen zu reduzieren: Die Anzahl erforderlicher Testzyklen bei Änderungen von G-Code oder Spezifikationen zu minimieren.
Autonome Fertigung zu ermöglichen: Eine mathematisch fundierte Grundlage für autonome, kollisionsärmere Fertigungssysteme zu schaffen.
Komplexität zu entkoppeln: Die Rechenlast kontinuierlicher Kinematik von der logischen Beweisführung zu trennen und formale Verifikation für komplexe industrielle Anwendungen handhabbar zu machen.

Die Autoren positionieren diese Arbeit nicht als Ersatz für alle Simulationen, sondern als eine rigorose, skalierbare Schicht, die sicherstellt, dass Sicherheitsvoraussetzungen erfüllt sind, bevor Zustandsübergänge erfolgen, und die mechanisierte Semantik aus anderen Bereichen wie der additiven Fertigung widerspiegelt. Zukünftige Arbeiten sollen „Incorrectness Separation Logic" zur Isolierung von Legacy-Fehlern und die Echtzeit-Integration in eingebettete Controller untersuchen.