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

Resumo Técnico: Feixes como Meio para Manter Consistência em Engenharia de Sistemas Baseada em Modelos

Declaração do Problema
Na Engenharia de Sistemas Baseada em Modelos (MBSE) para Sistemas Ciber-Físicos (CPS), as arquiteturas de sistemas são descritas por meio de múltiplas visões de engenharia sobrepostas (por exemplo, elétrica, térmica, mecânica, software). Um desafio metodológico central é garantir a consistência multivisão: que parâmetros e pressupostos em uma visão (por exemplo, dissipação de potência em um projeto elétrico) alinhem-se precisamente com restrições em outra (por exemplo, requisitos de dissipador de calor em um projeto térmico). As práticas atuais de MBSE dependem de revisões informais, matrizes de rastreabilidade e simulação. O artigo identifica duas deficiências críticas nessas abordagens:

1. Falta de Definição Semântica: Não há um critério matemático preciso definindo o que "consistência" significa ou quando uma família de projetos locais constitui um projeto global coerente.
2. Verificação Ineficiente: Os métodos existentes não isolam os dados específicos de compatibilidade local suficientes para garantir a consistência global, frequentemente levando a verificações redundantes ou insuficientes.

Metodologia
Os autores propõem um framework matemático que incorpora o problema de consistência multivisão na teoria de feixes. A metodologia procede em três etapas:

1. Construção de um Sítio Arquitetônico:

   • A estrutura do domínio de engenharia é modelada como um espaço topológico $X$ (o "sítio arquitetônico").
   • Pontos: Os pontos de $X$ são as interfaces pares entre domínios de engenharia (por exemplo, o acoplamento entre sistemas elétricos e mecânicos).
   • Conjuntos Abertos: Cada visão de engenharia (por exemplo, a visão "Elétrica") é definida como um conjunto aberto $U_k \subseteq X$ contendo todos os pontos de interface que envolvem essa visão.
   • Topologia: Para interfaces discretas finitas, o sítio é equipado com a topologia discreta.

2. Definição do Pré-feixe de Projeto:

   • Um pré-feixe de projeto $F$ é construído sobre $X$.
   • Para cada ponto de interface $x$, um tipo $P(x)$ representa o conjunto finito de parâmetros de acoplamento (escolhas de projeto) nessa interface.
   • Para qualquer conjunto aberto $U$ (uma visão), $F(U)$ é o produto dos tipos de parâmetros $\prod_{x \in U} P(x)$, representando o espaço de todos os projetos locais possíveis para essa visão.
   • Mapas de restrição correspondem a projeções, mapeando um projeto em uma visão maior para seus parâmetros em uma sub-visão (ou interface).

3. A Condição de Feixe como Consistência:

   • O artigo investiga se $F$ satisfaz a condição de feixe.
   • A condição de feixe exige que qualquer "família compatível" de projetos locais (projetos que concordam em suas sobreposições) possa ser "colada" para formar um projeto global único.
   • Os autores aproveitam um resultado clássico da teoria das categorias (Kashiwara–Schapira; Mac Lane–Moerdijk) e o formalizam em Lean 4 usando Mathlib: a condição de feixe é equivalente à condição de interseção par. Isso significa que a consistência global é garantida se e somente se os projetos forem compatíveis em todas as sobreposições pares.

Principais Contribuições

1. Incorporação Semântica: O artigo constrói uma incorporação semântica precisa do problema de consistência de engenharia na linguagem da teoria de feixes, definindo visões como conjuntos abertos e interfaces como pontos.
2. O Teorema de Consistência de Feixes: Os autores provam que, para um pré-feixe de projeto sobre um sítio arquitetônico, a condição de feixe (consistência global) é equivalente à condição de interseção par (compatibilidade local).
   • Teorema 1.1: $F$ é um feixe $\iff$ $F$ satisfaz a condição de interseção par.
3. Formalização Verificada por Máquina: Toda a construção, o teorema de equivalência e um exemplo prático concreto de três visões são formalizados e verificados por máquina em Lean 4. As provas são compiladas sem axiomas sorry, dependendo apenas de axiomas lógicos padrão.
4. Exemplo Prático Concreto: Uma instância específica envolvendo visões Elétrica, Térmica e Mecânica é formalizada, demonstrando como projetos locais compatíveis (por exemplo, parâmetros eletrotérmicos correspondentes) se colam em um projeto global único.

Resultados
A formalização estabelece três resultados primários:

• Equivalência: O pré-feixe de projeto é um feixe se e somente se satisfizer a compatibilidade de sobreposição par.
• Colagem: Projetos locais compatíveis determinam um projeto global único.
• Composicionalidade: Se um pré-feixe de projeto é um feixe e um funtor de propriedade $P$ (calculando quantidades derivadas como massa ou potência) preserva limites, então o pré-feixe composto $F \circ P$ também é um feixe. Isso garante que propriedades derivadas herdam automaticamente a garantia de consistência.

Significado e Alegações
O artigo alega que este framework fornece um critério rigoroso, do local para o global, para verificação de arquitetura:

• Redução da Complexidade de Verificação: A consistência global para $n$ visões pode ser certificada verificando apenas $\binom{n}{2}$ condições de interface par, em vez de verificações complexas multivias.
• Integração Determinística: Uma vez que os projetos locais são verificados como compatíveis em pares, o projeto do sistema global é unicamente determinado, transformando a fase de integração de uma tarefa criativa em uma etapa de montagem mecânica com correção garantida.
• Garantia Formal: A natureza verificada por máquina das provas oferece um nível de garantia superior ao das provas em papel, eliminando erros lógicos sutis e fornecendo uma base para futuras ferramentas de arquitetura certificadas.

Os autores posicionam este trabalho como a primeira formalização verificada por máquina da consistência multivisão baseada em teoria de feixes especificamente para arquitetura de CPS, distinguindo-o de trabalhos anteriores sobre operados (Spivak), profuntores de co-projeto (Censi) e alinhamento de ontologias (Breiner et al.) ao focar no acordo de parâmetros entre visões sobrepostas e não hierárquicas.