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

Technical Summary: Sheaves as a Means to Maintaining Consistency in Model-based Systems Engineering

Problem Statement
In Model-based Systems Engineering (MBSE) for Cyber-Physical Systems (CPS), system architectures are described through multiple, overlapping engineering views (e.g., electrical, thermal, mechanical, software). A central methodological challenge is ensuring multi-view consistency: that parameters and assumptions in one view (e.g., power dissipation in an electrical design) align precisely with constraints in another (e.g., heat sink requirements in a thermal design). Current MBSE practices rely on informal reviews, traceability matrices, and simulation. The paper identifies two critical deficiencies in these approaches:

1. Lack of Semantic Definition: There is no precise mathematical criterion defining what "consistency" means or when a family of local designs constitutes a coherent global design.
2. Inefficient Verification: Existing methods do not isolate the specific local compatibility data sufficient to guarantee global consistency, often leading to redundant or insufficient checks.

Methodology
The authors propose a mathematical framework embedding the multi-view consistency problem into sheaf theory. The methodology proceeds in three steps:

1. Construction of an Architectural Site:

   • The engineering domain structure is modeled as a topological space $X$ (the "architectural site").
   • Points: The points of $X$ are the pairwise interfaces between engineering domains (e.g., the coupling between electrical and mechanical systems).
   • Open Sets: Each engineering view (e.g., the "Electrical" view) is defined as an open set $U_k \subseteq X$ containing all interface points involving that view.
   • Topology: For finite discrete interfaces, the site is equipped with the discrete topology.

2. Definition of the Design Presheaf:

   • A design presheaf $F$ is constructed over $X$.
   • For each interface point $x$, a type $P(x)$ represents the finite set of coupling parameters (design choices) at that interface.
   • For any open set $U$ (a view), $F(U)$ is the product of parameter types $\prod_{x \in U} P(x)$, representing the space of all possible local designs for that view.
   • Restriction maps correspond to projections, mapping a design on a larger view to its parameters on a sub-view (or interface).

3. The Sheaf Condition as Consistency:

   • The paper investigates whether $F$ satisfies the sheaf condition.
   • The sheaf condition requires that any "compatible family" of local designs (designs that agree on their overlaps) can be "glued" to form a unique global design.
   • The authors leverage a classical result from category theory (Kashiwara–Schapira; Mac Lane–Moerdijk) and formalize it in Lean 4 using Mathlib: the sheaf condition is equivalent to the pairwise intersection condition. This means global consistency is guaranteed if and only if designs are compatible on all pairwise overlaps.

Key Contributions

1. Semantic Embedding: The paper constructs a precise semantic embedding of the engineering consistency problem into sheaf-theoretic language, defining views as open sets and interfaces as points.
2. The Sheaf Consistency Theorem: The authors prove that for a design presheaf over an architectural site, the sheaf condition (global consistency) is equivalent to the pairwise intersection condition (local compatibility).
   • Theorem 1.1: $F$ is a sheaf $\iff$ $F$ satisfies the pairwise intersection condition.
3. Machine-Verified Formalization: The entire construction, the equivalence theorem, and a concrete three-view worked example are formalized and machine-verified in Lean 4. The proofs compile without sorry axioms, relying only on standard logical axioms.
4. Concrete Worked Example: A specific instance involving Electrical, Thermal, and Mechanical views is formalized, demonstrating how compatible local designs (e.g., matching electro-thermal parameters) glue to a unique global design.

Results
The formalization establishes three primary results:

• Equivalence: The design presheaf is a sheaf if and only if it satisfies pairwise overlap compatibility.
• Gluing: Compatible local designs determine a unique global design.
• Compositionality: If a design presheaf is a sheaf, and a property functor $P$ (computing derived quantities like mass or power) preserves limits, then the composite presheaf $F \circ P$ is also a sheaf. This ensures that derived properties inherit the consistency guarantee automatically.

Significance and Claims
The paper claims that this framework provides a rigorous, local-to-global criterion for architecture verification:

• Reduction of Verification Complexity: Global consistency for $n$ views can be certified by checking only $\binom{n}{2}$ pairwise interface conditions, rather than complex multi-way checks.
• Deterministic Integration: Once local designs are verified as pairwise compatible, the global system design is uniquely determined, transforming the integration phase from a creative task into a mechanical assembly step with guaranteed correctness.
• Formal Assurance: The machine-verified nature of the proofs offers a higher level of assurance than paper proofs, eliminating subtle logical errors and providing a foundation for future certified architecture tools.

The authors position this work as the first machine-verified formalization of sheaf-theoretic multi-view consistency specifically for CPS architecture, distinguishing it from prior work on operads (Spivak), co-design profunctors (Censi), and ontology alignment (Breiner et al.) by focusing on parameter agreement across overlapping, non-hierarchical views.