Sheaves as a Means of Maintaining Consistency in Model-based Systems Engineering

Technische Zusammenfassung: Garben als Mittel zur Aufrechterhaltung der Konsistenz im modellbasierten Systems Engineering

Problemstellung
Im modellbasierten Systems Engineering (MBSE) für cyber-physische Systeme (CPS) werden Systemarchitekturen durch multiple, sich überschneidende ingenieurtechnische Sichtweisen (z. B. elektrisch, thermisch, mechanisch, softwaretechnisch) beschrieben. Eine zentrale methodische Herausforderung besteht darin, die Konsistenz über mehrere Sichtweisen sicherzustellen: Dass Parameter und Annahmen in einer Sichtweise (z. B. Leistungsverlust in einem elektrischen Entwurf) exakt mit den Randbedingungen in einer anderen (z. B. Anforderungen an den Kühlkörper in einem thermischen Entwurf) übereinstimmen. Die aktuellen MBSE-Praktiken verlassen sich auf informelle Reviews, Rückverfolgbarkeitsmatrizen und Simulationen. Die Arbeit identifiziert zwei kritische Mängel in diesen Ansätzen:

1. Fehlende semantische Definition: Es gibt kein präzises mathematisches Kriterium, das definiert, was „Konsistenz" bedeutet oder wann eine Familie lokaler Entwürfe einen kohärenten globalen Entwurf darstellt.
2. Ineffiziente Verifikation: Bestehende Methoden isolieren nicht die spezifischen lokalen Kompatibilitätsdaten, die ausreichen, um eine globale Konsistenz zu garantieren, was häufig zu redundanten oder unzureichenden Prüfungen führt.

Methodik
Die Autoren schlagen einen mathematischen Rahmen vor, der das Konsistenzproblem über mehrere Sichtweisen in die Garbentheorie einbettet. Die Methodik verläuft in drei Schritten:

1. Konstruktion eines architektonischen Ortes:

   • Die Struktur des ingenieurtechnischen Domänenbereichs wird als topologischer Raum $X$ (der „architektonische Ort") modelliert.
   • Punkte: Die Punkte von $X$ sind die paarweisen Schnittstellen zwischen ingenieurtechnischen Domänen (z. B. die Kopplung zwischen elektrischen und mechanischen Systemen).
   • Offene Mengen: Jede ingenieurtechnische Sichtweise (z. B. die Sichtweise „Elektrisch") wird als offene Menge $U_k \subseteq X$ definiert, die alle Schnittstellenpunkte enthält, die diese Sichtweise betreffen.
   • Topologie: Für endliche diskrete Schnittstellen ist der Ort mit der diskreten Topologie ausgestattet.

2. Definition des Entwurfs-Prägarben:

   • Über $X$ wird eine Entwurfs-Prägarbe $F$ konstruiert.
   • Für jeden Schnittstellenpunkt $x$ repräsentiert ein Typ $P(x)$ die endliche Menge der Kopplungsparameter (Entwurfsentscheidungen) an dieser Schnittstelle.
   • Für jede offene Menge $U$ (eine Sichtweise) ist $F(U)$ das Produkt der Parametertypen $\prod_{x \in U} P(x)$ und repräsentiert den Raum aller möglichen lokalen Entwürfe für diese Sichtweise.
   • Restriktionsabbildungen entsprechen Projektionen und bilden einen Entwurf auf einer größeren Sichtweise auf seine Parameter auf einer Teilsichtweise (oder Schnittstelle) ab.

3. Die Garbenbedingung als Konsistenz:

   • Die Arbeit untersucht, ob $F$ die Garbenbedingung erfüllt.
   • Die Garbenbedingung verlangt, dass jede „kompatible Familie" lokaler Entwürfe (Entwürfe, die in ihren Überschneidungen übereinstimmen) zu einem eindeutigen globalen Entwurf „verklebt" werden kann.
   • Die Autoren nutzen ein klassisches Ergebnis aus der Kategorientheorie (Kashiwara–Schapira; Mac Lane–Moerdijk) und formalisieren es in Lean 4 unter Verwendung von Mathlib: Die Garbenbedingung ist äquivalent zur Bedingung der paarweisen Schnittmenge. Dies bedeutet, dass globale Konsistenz genau dann garantiert ist, wenn Entwürfe auf allen paarweisen Überschneidungen kompatibel sind.

Hauptbeiträge

1. Semantische Einbettung: Die Arbeit konstruiert eine präzise semantische Einbettung des ingenieurtechnischen Konsistenzproblems in die garbentheoretische Sprache, wobei Sichtweisen als offene Mengen und Schnittstellen als Punkte definiert werden.
2. Der Garben-Konsistenzsatz: Die Autoren beweisen, dass für eine Entwurfs-Prägarbe über einem architektonischen Ort die Garbenbedingung (globale Konsistenz) äquivalent zur Bedingung der paarweisen Schnittmenge (lokale Kompatibilität) ist.
   • Satz 1.1: $F$ ist eine Garbe $\iff$ $F$ erfüllt die Bedingung der paarweisen Schnittmenge.
3. Maschinell verifizierte Formalisierung: Der gesamte Aufbau, der Äquivalenzsatz und ein konkretes durchgerechnetes Beispiel mit drei Sichtweisen wurden in Lean 4 formalisiert und maschinell verifiziert. Die Beweise kompilieren ohne sorry-Axiome und verlassen sich ausschließlich auf Standardlogik-Axiome.
4. Konkretes durchgerechnetes Beispiel: Ein spezifischer Fall, der die Sichtweisen Elektrisch, Thermisch und Mechanisch umfasst, wurde formalisiert und zeigt, wie kompatible lokale Entwürfe (z. B. übereinstimmende elektro-thermische Parameter) zu einem eindeutigen globalen Entwurf verklebt werden.

Ergebnisse
Die Formalisierung etabliert drei primäre Ergebnisse:

• Äquivalenz: Die Entwurfs-Prägarbe ist genau dann eine Garbe, wenn sie die paarweise Überschneidungskompatibilität erfüllt.
• Verklebung: Kompatible lokale Entwürfe bestimmen einen eindeutigen globalen Entwurf.
• Kompositionalität: Wenn eine Entwurfs-Prägarbe eine Garbe ist und ein Eigenschaftsfunktor $P$ (der abgeleitete Größen wie Masse oder Leistung berechnet) Limiten erhält, dann ist die zusammengesetzte Prägarbe $F \circ P$ ebenfalls eine Garbe. Dies stellt sicher, dass abgeleitete Eigenschaften die Konsistenzgarantie automatisch erben.

Bedeutung und Behauptungen
Die Arbeit behauptet, dass dieser Rahmen ein rigoroses, vom Lokalen zum Globalen reichendes Kriterium für die Architekturverifikation bietet:

• Reduktion der Verifikationskomplexität: Globale Konsistenz für $n$ Sichtweisen kann durch Prüfung von nur $\binom{n}{2}$ paarweisen Schnittstellenbedingungen zertifiziert werden, anstatt komplexe Mehrweg-Prüfungen durchzuführen.
• Deterministische Integration: Sobald lokale Entwürfe als paarweise kompatibel verifiziert sind, ist das globale Systemdesign eindeutig bestimmt; dies verwandelt die Integrationsphase von einer kreativen Aufgabe in einen mechanischen Montageschritt mit garantierter Korrektheit.
• Formale Absicherung: Der maschinell verifizierte Charakter der Beweise bietet ein höheres Maß an Absicherung als Papierbeweise, eliminiert subtile logische Fehler und bildet eine Grundlage für zukünftige zertifizierte Architekturtouls.

Die Autoren positionieren diese Arbeit als die erste maschinell verifizierte Formalisierung der garbentheoretischen Konsistenz über mehrere Sichtweisen speziell für CPS-Architekturen. Sie unterscheidet sich von früheren Arbeiten zu Operaden (Spivak), Co-Design-Profunctoren (Censi) und Ontologie-Alignment (Breiner et al.) durch den Fokus auf Parameterübereinstimmung über sich überschneidende, nicht-hierarchische Sichtweisen hinweg.