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

Résumé technique : Les faisceaux comme moyen de maintenir la cohérence dans l'ingénierie des systèmes basée sur les modèles

Énoncé du problème
Dans l'ingénierie des systèmes basée sur les modèles (MBSE) pour les systèmes cyber-physiques (CPS), les architectures de systèmes sont décrites à travers plusieurs vues d'ingénierie qui se chevauchent (par exemple, électrique, thermique, mécanique, logiciel). Un défi méthodologique central consiste à assurer la cohérence multi-vues : que les paramètres et les hypothèses dans une vue (par exemple, la dissipation de puissance dans une conception électrique) s'alignent précisément avec les contraintes dans une autre (par exemple, les exigences de dissipateur thermique dans une conception thermique). Les pratiques actuelles de MBSE reposent sur des revues informelles, des matrices de traçabilité et des simulations. L'article identifie deux lacunes critiques dans ces approches :

1. Absence de définition sémantique : Il n'existe aucun critère mathématique précis définissant ce que signifie la « cohérence » ou lorsqu'une famille de conceptions locales constitue une conception globale cohérente.
2. Vérification inefficace : Les méthodes existantes n'isolent pas les données de compatibilité locales spécifiques suffisantes pour garantir la cohérence globale, conduisant souvent à des vérifications redondantes ou insuffisantes.

Méthodologie
Les auteurs proposent un cadre mathématique intégrant le problème de la cohérence multi-vues dans la théorie des faisceaux. La méthodologie procède en trois étapes :

1. Construction d'un site architectural :

   • La structure du domaine d'ingénierie est modélisée comme un espace topologique $X$ (le « site architectural »).
   • Points : Les points de $X$ sont les interfaces deux à deux entre les domaines d'ingénierie (par exemple, le couplage entre les systèmes électriques et mécaniques).
   • Ouverts : Chaque vue d'ingénierie (par exemple, la vue « Électrique ») est définie comme un ouvert $U_k \subseteq X$ contenant tous les points d'interface impliquant cette vue.
   • Topologie : Pour des interfaces discrètes finies, le site est équipé de la topologie discrète.

2. Définition du préfaisceau de conception :

   • Un préfaisceau de conception $F$ est construit sur $X$.
   • Pour chaque point d'interface $x$, un type $P(x)$ représente l'ensemble fini des paramètres de couplage (choix de conception) à cette interface.
   • Pour tout ouvert $U$ (une vue), $F(U)$ est le produit des types de paramètres $\prod_{x \in U} P(x)$, représentant l'espace de toutes les conceptions locales possibles pour cette vue.
   • Les applications de restriction correspondent aux projections, mappant une conception sur une vue plus large vers ses paramètres sur une sous-vue (ou interface).

3. La condition de faisceau comme cohérence :

   • L'article examine si $F$ satisfait la condition de faisceau.
   • La condition de faisceau exige que toute « famille compatible » de conceptions locales (conceptions qui s'accordent sur leurs chevauchements) puisse être « collée » pour former une conception globale unique.
   • Les auteurs exploitent un résultat classique de la théorie des catégories (Kashiwara–Schapira ; Mac Lane–Moerdijk) et le formalisent en Lean 4 utilisant Mathlib : la condition de faisceau est équivalente à la condition d'intersection deux à deux. Cela signifie que la cohérence globale est garantie si et seulement si les conceptions sont compatibles sur tous les chevauchements deux à deux.

Contributions clés

1. Intégration sémantique : L'article construit une intégration sémantique précise du problème de cohérence en ingénierie dans le langage de la théorie des faisceaux, définissant les vues comme des ouverts et les interfaces comme des points.
2. Le théorème de cohérence des faisceaux : Les auteurs prouvent que pour un préfaisceau de conception sur un site architectural, la condition de faisceau (cohérence globale) est équivalente à la condition d'intersection deux à deux (compatibilité locale).
   • Théorème 1.1 : $F$ est un faisceau $\iff$ $F$ satisfait la condition d'intersection deux à deux.
3. Formalisation vérifiée par machine : Toute la construction, le théorème d'équivalence et un exemple concret traité à trois vues sont formalisés et vérifiés par machine en Lean 4. Les preuves se compilent sans axiomes sorry, reposant uniquement sur des axiomes logiques standards.
4. Exemple concret traité : Une instance spécifique impliquant les vues Électrique, Thermique et Mécanique est formalisée, démontrant comment des conceptions locales compatibles (par exemple, des paramètres électro-thermiques correspondants) se collent en une conception globale unique.

Résultats
La formalisation établit trois résultats principaux :

• Équivalence : Le préfaisceau de conception est un faisceau si et seulement s'il satisfait la compatibilité de chevauchement deux à deux.
• Collage : Des conceptions locales compatibles déterminent une conception globale unique.
• Compositionnalité : Si un préfaisceau de conception est un faisceau, et qu'un foncteur de propriété $P$ (calculant des grandeurs dérivées comme la masse ou la puissance) préserve les limites, alors le préfaisceau composé $F \circ P$ est également un faisceau. Cela garantit que les propriétés dérivées héritent automatiquement de la garantie de cohérence.

Signification et affirmations
L'article affirme que ce cadre fournit un critère rigoureux, du local au global, pour la vérification d'architecture :

• Réduction de la complexité de vérification : La cohérence globale pour $n$ vues peut être certifiée en vérifiant uniquement $\binom{n}{2}$ conditions d'interface deux à deux, plutôt que des vérifications multi-voies complexes.
• Intégration déterministe : Une fois que les conceptions locales sont vérifiées comme compatibles deux à deux, la conception du système global est déterminée de manière unique, transformant la phase d'intégration d'une tâche créative en une étape d'assemblage mécanique avec une correction garantie.
• Assurance formelle : La nature vérifiée par machine des preuves offre un niveau d'assurance supérieur aux preuves papier, éliminant les erreurs logiques subtiles et fournissant une fondation pour de futurs outils d'architecture certifiés.

Les auteurs positionnent ce travail comme la première formalisation vérifiée par machine de la cohérence multi-vues fondée sur la théorie des faisceaux spécifiquement pour l'architecture CPS, la distinguant des travaux antérieurs sur les opérades (Spivak), les profoncteurs de co-conception (Censi) et l'alignement d'ontologies (Breiner et al.) en se concentrant sur l'accord des paramètres à travers des vues chevauchantes et non hiérarchiques.