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

TL;DR

This paper models multi-view consistency in cyber-physical systems using sheaf theory, formalizing the process of ensuring local compatibility leads to a unique global design, with machine-verified proofs in Lean 4.

Contribution

It introduces a sheaf-theoretic framework for formalizing and verifying multi-view consistency in model-based systems engineering, with machine-verified proofs.

Findings

Sheaf condition is equivalent to pairwise overlap compatibility.

Compatible local designs uniquely determine a global design.

Machine-verified formalization in Lean 4 confirms the theoretical results.

Abstract

We propose that the sheaf condition on a presheaf of design spaces provides a mathematical model for multi-view consistency in the architecture of cyber-physical systems (CPS). In model-based systems engineering, multiple engineering views -- electrical, thermal, mechanical, and software -- must be kept mutually consistent, yet current practice relies on informal procedures without a precise semantic account of global consistency. We construct an architectural site: a topological space whose points are pairwise interfaces between engineering domains and whose open sets represent engineering views. A design presheaf assigns to each view its local design space and to each inclusion the corresponding restriction map. We show that the sheaf condition on this presheaf is equivalent to compatibility on pairwise overlaps, yielding a local criterion for global multi-view consistency. The equivalence and a concrete three-view worked example are machine-verified in Lean 4 using Mathlib. The formalization establishes that the design presheaf is a sheaf, that the sheaf condition is equivalent to pairwise overlap compatibility, and that compatible local design families glue to unique global designs. Global consistency of an arbitrary number of views can be certified by checking only pairwise interface compatibility; compatible local designs determine a unique global design; derived properties computed by limit-preserving functors inherit the same consistency guarantee; and the entire verification chain admits machine-checkable proofs in Lean.