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

Resumen Técnico: Hazos como Medio para Mantener la Consistencia en la Ingeniería de Sistemas Basada en Modelos

Enunciado del Problema
En la Ingeniería de Sistemas Basada en Modelos (MBSE) para Sistemas Ciberfísicos (CPS), las arquitecturas de los sistemas se describen mediante múltiples vistas de ingeniería superpuestas (por ejemplo, eléctrica, térmica, mecánica, software). Un desafío metodológico central es garantizar la consistencia multi-vista: que los parámetros y supuestos en una vista (por ejemplo, la disipación de potencia en un diseño eléctrico) coincidan exactamente con las restricciones en otra (por ejemplo, los requisitos del disipador de calor en un diseño térmico). Las prácticas actuales de MBSE dependen de revisiones informales, matrices de trazabilidad y simulación. El artículo identifica dos deficiencias críticas en estos enfoques:

1. Falta de Definición Semántica: No existe un criterio matemático preciso que defina qué significa "consistencia" o cuándo una familia de diseños locales constituye un diseño global coherente.
2. Verificación Ineficiente: Los métodos existentes no aíslan los datos específicos de compatibilidad local suficientes para garantizar la consistencia global, lo que a menudo conduce a verificaciones redundantes o insuficientes.

Metodología
Los autores proponen un marco matemático que incrusta el problema de la consistencia multi-vista en la teoría de haces. La metodología procede en tres pasos:

1. Construcción de un Sitio Arquitectónico:

   • La estructura del dominio de ingeniería se modela como un espacio topológico $X$ (el "sitio arquitectónico").
   • Puntos: Los puntos de $X$ son las interfases por pares entre dominios de ingeniería (por ejemplo, el acoplamiento entre sistemas eléctricos y mecánicos).
   • Conjuntos Abiertos: Cada vista de ingeniería (por ejemplo, la vista "Eléctrica") se define como un conjunto abierto $U_k \subseteq X$ que contiene todos los puntos de interfase que involucran dicha vista.
   • Topología: Para interfases discretas finitas, el sitio se equipa con la topología discreta.

2. Definición del Prehaz de Diseño:

   • Se construye un prehaz de diseño $F$ sobre $X$.
   • Para cada punto de interfase $x$, un tipo $P(x)$ representa el conjunto finito de parámetros de acoplamiento (elecciones de diseño) en esa interfase.
   • Para cualquier conjunto abierto $U$ (una vista), $F(U)$ es el producto de los tipos de parámetros $\prod_{x \in U} P(x)$, que representa el espacio de todos los diseños locales posibles para esa vista.
   • Las aplicaciones de restricción corresponden a proyecciones, mapeando un diseño en una vista más grande hacia sus parámetros en una sub-vista (o interfase).

3. La Condición de Haz como Consistencia:

   • El artículo investiga si $F$ satisface la condición de haz.
   • La condición de haz requiere que cualquier "familia compatible" de diseños locales (diseños que coinciden en sus superposiciones) pueda "pegarse" para formar un diseño global único.
   • Los autores aprovechan un resultado clásico de la teoría de categorías (Kashiwara–Schapira; Mac Lane–Moerdijk) y lo formalizan en Lean 4 utilizando Mathlib: la condición de haz es equivalente a la condición de intersección por pares. Esto significa que la consistencia global está garantizada si y solo si los diseños son compatibles en todas las superposiciones por pares.

Contribuciones Clave

1. Incrustación Semántica: El artículo construye una incrustación semántica precisa del problema de consistencia de ingeniería en el lenguaje de la teoría de haces, definiendo las vistas como conjuntos abiertos y las interfases como puntos.
2. El Teorema de Consistencia de Hazos: Los autores demuestran que, para un prehaz de diseño sobre un sitio arquitectónico, la condición de haz (consistencia global) es equivalente a la condición de intersección por pares (compatibilidad local).
   • Teorema 1.1: $F$ es un haz $\iff$ $F$ satisface la condición de intersección por pares.
3. Formalización Verificada por Máquina: Toda la construcción, el teorema de equivalencia y un ejemplo trabajado concreto de tres vistas se formalizan y verifican mediante máquina en Lean 4. Las pruebas se compilan sin axiomas sorry, dependiendo únicamente de axiomas lógicos estándar.
4. Ejemplo Trabajado Concreto: Se formaliza una instancia específica que involucra las vistas Eléctrica, Térmica y Mecánica, demostrando cómo los diseños locales compatibles (por ejemplo, parámetros electro-térmicos coincidentes) se pegan en un diseño global único.

Resultados
La formalización establece tres resultados principales:

• Equivalencia: El prehaz de diseño es un haz si y solo si satisface la compatibilidad de superposición por pares.
• Pegado: Los diseños locales compatibles determinan un diseño global único.
• Composicionalidad: Si un prehaz de diseño es un haz, y un funtor de propiedad $P$ (que calcula cantidades derivadas como masa o potencia) preserva límites, entonces el prehaz compuesto $F \circ P$ también es un haz. Esto garantiza que las propiedades derivadas heredan automáticamente la garantía de consistencia.

Significado y Afirmaciones
El artículo afirma que este marco proporciona un criterio riguroso, de lo local a lo global, para la verificación de arquitecturas:

• Reducción de la Complejidad de Verificación: La consistencia global para $n$ vistas puede certificarse verificando solo $\binom{n}{2}$ condiciones de interfase por pares, en lugar de verificaciones complejas de múltiples vías.
• Integración Determinista: Una vez que los diseños locales se verifican como compatibles por pares, el diseño del sistema global queda determinado de manera única, transformando la fase de integración de una tarea creativa en un paso de ensamblaje mecánico con corrección garantizada.
• Garantía Formal: La naturaleza verificada por máquina de las pruebas ofrece un nivel de garantía superior al de las pruebas en papel, eliminando errores lógicos sutiles y proporcionando una base para futuras herramientas de arquitectura certificadas.

Los autores posicionan este trabajo como la primera formalización verificada por máquina de la consistencia multi-vista basada en teoría de haces específicamente para la arquitectura de CPS, distinguiéndola de trabajos anteriores sobre operadas (Spivak), profuntores de co-diseño (Censi) y alineación de ontologías (Breiner et al.) al centrarse en el acuerdo de parámetros a través de vistas superpuestas y no jerárquicas.