Capítulo 2 — Matemática discreta
Mapa da aula
Aula 02 publicada. Mapa, exemplo, EX003.
flowchart TD
N0["2.1 A lógica é a linguagem das permissões"]
N1["2.2 Grafos modelam dependência"]
N2["2.5 Atividade prática: Laboratório 2"]
N3["Síntese do capítulo"]
N0 --> N1 --> N2 --> N3
N3 --> EX["Exemplo resolvido"]
EX --> Q["Exercício EX003"]
Desenho lógico
flowchart LR
N0["2.1 A lógica é a linguagem das permissões"]
N1["2.2 Grafos modelam dependência"]
N2["2.5 Atividade prática: Laboratório 2"]
N3["Síntese do capítulo"]
N0 --> N1 --> N2 --> N3 --> Q["EX003"]
[2.1 A lógica é a linguagem das permissões]
|
v
[2.2 Grafos modelam dependência]
|
v
[2.5 Atividade prática: Laboratório 2]
|
v
[Síntese do capítulo]
|
v
[Exemplo resolvido] --> [Exercício EX003]
Objetivos de aprendizagem e conexão
Ao fim deste capítulo você será capaz de (1) escrever condições de intertravamento e de permissão como expressões booleanas e verificá-las exaustivamente com uma tabela-verdade; (2) modelar dependências de infraestrutura como um grafo dirigido e calcular o que falha quando um nó falha; (3) usar conjuntos, relações e contagem para limitar quantos estados um sistema de controle pode assumir; e (4) dizer com precisão quando uma verificação exaustiva é viável e quando não é. O capítulo se apoia na visão de estoques e fluxos do Capítulo 1 e prepara o Capítulo 4, em que você vai implementar esses modelos em código.
2.1 A lógica é a linguagem das permissões
Sistemas de controle estão cheios de regras da forma "a bomba só pode funcionar se…". Escreva-as como expressões booleanas. Seja $H$ = nível acima do limite alto, $S$ = pressão de sucção baixa, $P$ = permissão remota presente, $M$ = modo manual local selecionado. Uma regra típica é $\text{RUN} = \neg H \wedge \neg S \wedge (P \vee M)$. Duas regras são equivalentes se concordam em todas as entradas; as leis de De Morgan ($\neg(A\wedge B) = \neg A \vee \neg B$) permitem reescrever condições de desarme como permissões. Com quatro entradas há $2^4 = 16$ estados, e uma tabela-verdade verifica cada um deles. A engenharia de segurança acrescenta uma pergunta que a engenharia de segurança operacional já faz: em que entrada um atacante pode influir? Se $P$ chega por uma rede, então $P \vee M$ significa que uma permissão forjada basta para ligar a bomba sempre que $H$ e $S$ forem falsos. Isso pode ser aceitável — os desarmes físicos continuam valendo — ou não, se funcionar naquele momento causar um transiente de pressão.
2.2 Grafos modelam dependência
Um grafo dirigido $G = (V, E)$ tem nós e setas. Desenhe uma seta de $a$ para $b$ quando $a$ precisa de $b$ para funcionar. O conjunto do que é afetado quando $b$ falha é tudo o que consegue chegar a $b$ seguindo as setas — seus ancestrais nessa orientação. A busca em largura calcula esse conjunto em tempo proporcional ao número de arestas. Rinaldi, Peerenboom and Kelly (2001) distinguem interdependências físicas, cibernéticas, geográficas e lógicas entre infraestruturas; um grafo de dependências é o modelo mais simples capaz de conter as quatro, desde que você rotule cada aresta com seu tipo.
Vocabulário de grafos que você vai usar: caminho, ciclo (um laço de dependência — por exemplo, a rede de telemetria precisa da energia da rede elétrica, e a recomposição feita pelo operador da rede elétrica precisa da telemetria), grau de entrada e grau de saída, vértice de corte (um nó cuja remoção desconecta o grafo) e componente fortemente conexa. Um vértice de corte num grafo de abastecimento é um ponto único de falha.
2.3 Contagem, espaços de estados e seus limites
Um sistema com $n$ entradas binárias tem $2^n$ estados de entrada; com 30 entradas, são mais de um bilhão. Acrescente memória interna (temporizadores, travas) e o espaço de estados cresce mais depressa. A verificação exaustiva é excelente para pequenos intertravamentos e impossível para plantas inteiras; para estas, você usa estrutura (decomposição, invariantes) e amostragem (Capítulo 30). O princípio da casa dos pombos dá limites rápidos de segurança: um contador de mensagens de 16 bits dá a volta após 65.536 mensagens, então, a uma mensagem por segundo, ele se repete em cerca de 18 horas, e a partir daí uma verificação contra repetição baseada apenas nesse contador falha.
2.4 Exemplo resolvido: dependências de Lowmarsh (sintético)
Os engenheiros da LRWA listam aquilo de que depende o abastecimento do St Brenna's Hospital: o reservatório de Hollin Hill e a alimentação direta pela PS4; Hollin Hill depende da PS3; cada estação de bombeamento precisa da energia da rede elétrica e de sua RTU; as duas RTUs se comunicam por uma rede LTE privada que, por sua vez, é alimentada pelo alimentador F1 da rede elétrica. O Laboratório 2 codifica isso e calcula o conjunto de impacto de cada falha. Perder o alimentador F1 derruba a rede LTE além da PS3 — e assim a telemetria "redundante" da PS4, que está no alimentador F2, também se perde. O projeto com dois alimentadores parecia diverso no desenho elétrico; o grafo mostra uma dependência comum pelas comunicações.
2.5 Atividade prática: Laboratório 2
# Lab 2 - dependency closure and an interlock truth table (synthetic Lowmarsh assets, offline)
from collections import deque
from itertools import product
DEPENDS = { # asset: assets it needs in order to work
"hospital_supply": ["hollin_res", "ps4"],
"hollin_res": ["ps3"], "ps4": ["grid_f2", "rtu4"], "ps3": ["grid_f1", "rtu3"],
"rtu3": ["lte"], "rtu4": ["lte"], "lte": ["grid_f1"], "fenwick_wtw": ["grid_f1", "chlorine"],
"ps3_feed": ["fenwick_wtw"],
}
def impacted(failed):
users = {}
for a, ds in DEPENDS.items():
for d in ds: users.setdefault(d, []).append(a)
seen, q = {failed}, deque([failed])
while q:
n = q.popleft()
for u in users.get(n, []):
if u not in seen: seen.add(u); q.append(u)
return sorted(seen - {failed})
for f in ("grid_f1", "lte", "grid_f2", "chlorine"):
print(f"{f:9} -> {impacted(f)}")
# Pump P3 may run iff level below high AND suction not low AND (remote permit OR local manual)
rows = [(h, s, p, m, (not h) and (not s) and (p or m)) for h, s, p, m in product([0, 1], repeat=4)]
print("states allowing run:", sum(r[4] for r in rows), "of", len(rows))
Saída esperada:
grid_f1 -> ['fenwick_wtw', 'hollin_res', 'hospital_supply', 'lte', 'ps3', 'ps3_feed', 'ps4', 'rtu3', 'rtu4']
lte -> ['hollin_res', 'hospital_supply', 'ps3', 'ps4', 'rtu3', 'rtu4']
grid_f2 -> ['hospital_supply', 'ps4']
chlorine -> ['fenwick_wtw', 'ps3_feed']
states allowing run: 3 of 16
Apenas 3 dos 16 estados de entrada permitem que a bomba funcione: aqueles com $H = S = 0$ e pelo menos um entre $P, M$.
Leia devagar a lista de impacto do alimentador F1. Ela contém a rede LTE, as duas RTUs e a PS4, embora a própria PS4 seja alimentada pelo alimentador F2, porque a RTU da PS4 só chega à sala de controle pela LTE. Essa é a dependência comum oculta que o exemplo resolvido descreve. O resultado da tabela-verdade é igualmente concreto: três de dezesseis estados permitem que a bomba funcione, e todos eles exigem que as entradas de nível alto e de sucção baixa sejam falsas, então uma permissão remota forjada sozinha nunca consegue ligar a bomba numa condição de desarme.
2.6 Erros comuns e limites
- Desenhar setas em direções misturadas ("alimenta" versus "depende de") num mesmo grafo.
- Tratar dois caminhos como redundantes sem verificar nós compartilhados mais adiante.
- Testar um intertravamento apenas com casos "típicos", quando a tabela é pequena o bastante para testar todos.
- Esquecer que um grafo modela se algo funciona, e não quão bem: modos degradados precisam de pesos ou de estados (Capítulo 22).
- Escolher tamanhos de contadores e de identificadores sem contar quanto tempo falta até darem a volta.
Na LRWA esses erros têm consequências diretas: um grafo que mistura direções de setas informaria que perder a PS4 prejudica o alimentador F2, e uma revisão que parasse no desenho elétrico teria deixado passar completamente a dependência compartilhada da LTE.
Exercícios — capítulo 2
EX003 — Reescrita do intertravamento. Objetivo: manipular expressões booleanas e raciocinar sobre entradas que chegam pela rede. Entradas: RUN na §2.1. Passos: (1) escreva a condição de desarme $\neg\text{RUN}$ na forma de soma de produtos usando as leis de De Morgan; (2) liste os estados em que uma permissão remota forjada muda o resultado; (3) proponha uma mudança que mantenha a operação remota, mas exija uma segunda condição independente. Evidência esperada: expressões, lista e proposta. Rubrica: 3 = álgebra correta, exatamente os estados certos, proposta independente do mesmo caminho de rede; 2 = um deslize; 1 = apenas a álgebra; 0 = nada.
EX004 — Verificação de diversidade. Objetivo: encontrar dependências comuns ocultas. Entradas: Laboratório 2. Passos: (1) acrescente um enlace por satélite com bateria, sat, usado apenas pela RTU4, sem dependência da rede elétrica; (2) execute de novo e informe o impacto de grid_f1; (3) diga se o abastecimento do hospital agora sobrevive à perda de F1 e o que o grafo ainda não lhe diz. Evidência esperada: dicionário modificado, saída, duas frases. Rubrica: 3 = modelagem correta (a RTU4 depender de lte ou de sat exige observar que este grafo simples só modela dependências do tipo E), conclusão honesta sobre esse limite; 2 = saída correta, limite não percebido; 1 = não executado; 0 = nada.
Síntese do capítulo
Escreva regras como lógica e dependências como grafos, e depois deixe o computador verificá-las. Pequenos intertravamentos podem e devem ser verificados exaustivamente; sistemas inteiros não podem, e a contagem lhe diz isso. Procure nós compartilhados por trás de caminhos aparentemente diversos, rotule as arestas com seu tipo e pergunte, para cada entrada, quais delas chegam por uma rede que um adversário pode alcançar.
Continue estudando — capítulo 02 de 50
← Capítulo 01 · Índice de capítulos do curso · Capítulo 03 →
Siga para a próxima lição escrita.