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

Riepilogo Tecnico: I Fasci come Mezzo per Mantenere la Coerenza nei Sistemi di Ingegneria Basati su Modelli

Enunciazione del Problema
Nell'Ingegneria dei Sistemi Basata su Modelli (MBSE) per Sistemi Cyber-Fisici (CPS), le architetture di sistema sono descritte attraverso molteplici viste ingegneristiche sovrapposte (ad esempio, elettrica, termica, meccanica, software). Una sfida metodologica centrale è garantire la coerenza multi-vista: che i parametri e le assunzioni in una vista (ad esempio, la dissipazione di potenza in un progetto elettrico) corrispondano esattamente ai vincoli in un'altra (ad esempio, i requisiti del dissipatore di calore in un progetto termico). Le attuali pratiche MBSE si affidano a revisioni informali, matrici di tracciabilità e simulazioni. Il documento individua due carenze critiche in questi approcci:

1. Mancanza di Definizione Semantica: Non esiste un criterio matematico preciso che definisca cosa significhi "coerenza" o quando una famiglia di progetti locali costituisca un progetto globale coerente.
2. Verifica inefficiente: I metodi esistenti non isolano i dati specifici di compatibilità locale sufficienti a garantire la coerenza globale, portando spesso a controlli ridondanti o insufficienti.

Metodologia
Gli autori propongono un quadro matematico che incorpora il problema della coerenza multi-vista nella teoria dei fasci. La metodologia procede in tre passaggi:

1. Costruzione di un Sito Architettonico:

   • La struttura del dominio ingegneristico è modellata come uno spazio topologico $X$ (il "sito architettonico").
   • Punti: I punti di $X$ sono le interfacce a coppie tra i domini ingegneristici (ad esempio, l'accoppiamento tra sistemi elettrici e meccanici).
   • Insiemi Aperti: Ogni vista ingegneristica (ad esempio, la vista "Elettrica") è definita come un insieme aperto $U_k \subseteq X$ contenente tutti i punti di interfaccia che coinvolgono tale vista.
   • Topologia: Per interfacce discrete finite, il sito è dotato della topologia discreta.

2. Definizione del Prefascio di Progetto:

   • Viene costruito un prefascio di progetto $F$ su $X$.
   • Per ogni punto di interfaccia $x$, un tipo $P(x)$ rappresenta l'insieme finito dei parametri di accoppiamento (scelte di progetto) in quell'interfaccia.
   • Per qualsiasi insieme aperto $U$ (una vista), $F(U)$ è il prodotto dei tipi di parametri $\prod_{x \in U} P(x)$, che rappresenta lo spazio di tutti i possibili progetti locali per quella vista.
   • Le mappe di restrizione corrispondono a proiezioni, mappando un progetto su una vista più ampia ai suoi parametri su una sotto-vista (o interfaccia).

3. La Condizione di Fascio come Coerenza:

   • Il documento indaga se $F$ soddisfi la condizione di fascio.
   • La condizione di fascio richiede che qualsiasi "famiglia compatibile" di progetti locali (progetti che concordano sulle loro sovrapposizioni) possa essere "incollata" per formare un progetto globale unico.
   • Gli autori sfruttano un risultato classico della teoria delle categorie (Kashiwara–Schapira; Mac Lane–Moerdijk) e lo formalizzano in Lean 4 utilizzando Mathlib: la condizione di fascio è equivalente alla condizione di intersezione a coppie. Ciò significa che la coerenza globale è garantita se e solo se i progetti sono compatibili su tutte le sovrapposizioni a coppie.

Contributi Chiave

1. Incorporamento Semantico: Il documento costruisce un incorporamento semantico preciso del problema della coerenza ingegneristica nel linguaggio della teoria dei fasci, definendo le viste come insiemi aperti e le interfacce come punti.
2. Il Teorema di Coerenza del Fascio: Gli autori dimostrano che per un prefascio di progetto su un sito architettonico, la condizione di fascio (coerenza globale) è equivalente alla condizione di intersezione a coppie (compatibilità locale).
   • Teorema 1.1: $F$ è un fascio $\iff$ $F$ soddisfa la condizione di intersezione a coppie.
3. Formalizzazione Verificata da Macchina: L'intera costruzione, il teorema di equivalenza e un esempio concreto risolto a tre viste sono formalizzati e verificati da macchina in Lean 4. Le prove vengono compilate senza assiomi sorry, affidandosi solo agli assiomi logici standard.
4. Esempio Concreto Risolto: Viene formalizzata un'istanza specifica che coinvolge le viste Elettrica, Termica e Meccanica, dimostrando come progetti locali compatibili (ad esempio, parametri elettro-termici corrispondenti) si incollino in un progetto globale unico.

Risultati
La formalizzazione stabilisce tre risultati principali:

• Equivalenza: Il prefascio di progetto è un fascio se e solo se soddisfa la compatibilità delle sovrapposizioni a coppie.
• Incollaggio: I progetti locali compatibili determinano un progetto globale unico.
• Composizionalità: Se un prefascio di progetto è un fascio e un funtore proprietà $P$ (che calcola quantità derivate come massa o potenza) preserva i limiti, allora il prefascio composito $F \circ P$ è anch'esso un fascio. Ciò garantisce che le proprietà derivate ereditino automaticamente la garanzia di coerenza.

Significato e Affermazioni
Il documento afferma che questo quadro fornisce un criterio rigoroso, dal locale al globale, per la verifica dell'architettura:

• Riduzione della Complessità di Verifica: La coerenza globale per $n$ viste può essere certificata controllando solo $\binom{n}{2}$ condizioni di interfaccia a coppie, piuttosto che controlli multipli complessi.
• Integrazione Deterministica: Una volta verificati i progetti locali come compatibili a coppie, il progetto del sistema globale è univocamente determinato, trasformando la fase di integrazione da un compito creativo in un passo di assemblaggio meccanico con correttezza garantita.
• Assicurazione Formale: La natura verificata da macchina delle prove offre un livello di assicurazione superiore rispetto alle prove cartacee, eliminando errori logici sottili e fornendo una base per futuri strumenti di architettura certificati.

Gli autori posizionano questo lavoro come la prima formalizzazione verificata da macchina della coerenza multi-vista basata sulla teoria dei fasci specificamente per l'architettura CPS, distinguendosi dai lavori precedenti su operadi (Spivak), profunctori di co-design (Censi) e allineamento di ontologie (Breiner et al.) concentrandosi sull'accordo dei parametri attraverso viste sovrapposte e non gerarchiche.