Sistemas Criticos: Como Software de Aviao,

O que torna um software 'critico'

Software critico e qualquer software cuja falha pode causar morte, lesao grave, dano ambiental significativo ou perda financeira catastrofica. Nao e uma definicao arbitraria — existem padroes internacionais que classificam software por nivel de criticidade.

A classificacao mais comum usa o conceito de Safety Integrity Level (SIL), que vai de 1 (menos critico) a 4 (mais critico). SIL 4 e reservado pra sistemas onde uma falha causa 'multiplas fatalidades' — think controle de reatores nucleares ou sistemas de frenagem de trens.

A diferenca entre software critico e o seu SaaS nao e a linguagem de programacao ou a stack. E o processo. Em software critico, cada linha de codigo precisa ter rastreabilidade ate um requisito de seguranca. Cada mudanca precisa de analise de impacto formal. Cada teste precisa provar que o software nao faz coisas que nao deveria fazer — nao so que faz o que deveria.

Parece burocracia? E. Mas e burocracia que salva vidas. O Boeing 737 MAX mostrou o que acontece quando voce relaxa esses processos num sistema critico — 346 pessoas morreram.

DO-178C: como avioes voam com software

O DO-178C e o padrao que rege o desenvolvimento de software para aviacao. Publicado pela RTCA, e reconhecido pela FAA (EUA) e EASA (Europa). Se voce quer colocar software dentro de um aviao, precisa seguir o DO-178C. Nao tem opcao B.

O padrao define 5 niveis de criticidade chamados Design Assurance Levels (DAL), de A (catastrofico) a E (sem impacto na seguranca). O nivel muda radicalmente a quantidade de trabalho exigida.

No DAL A, voce precisa de MC/DC (Modified Condition/Decision Coverage). Isso significa que cada condicao individual em cada decisao do codigo precisa ser testada de forma que mostre influencia independente no resultado. Nao basta testar 'if (a && b)' com true/true e false/false. Voce precisa testar cada variavel individualmente pra provar que ela afeta o resultado.

Pra ter ideia do custo: estima-se que software DAL A custa entre 50 e 100 dolares por linha de codigo. Um modulo com 10 mil linhas pode custar 1 milhao de dolares so de verificacao e certificacao. E por isso que reusar modulos certificados e tao atraente na aviacao — e tambem por que o reuso sem auditoria e tao perigoso.

ECSS: software que vai pro espaco

Na industria espacial europeia, o padrao e o ECSS (European Cooperation for Space Standardization), especificamente o ECSS-E-ST-40C pra engenharia de software. A ESA (Agencia Espacial Europeia) usa esse padrao em todos os seus projetos — incluindo, ironicamente, os que vieram depois do Ariane 5.

O ECSS e mais rigido que o DO-178C em alguns aspectos. Software espacial tem um problema extra: voce nao pode fazer hotfix depois do lancamento. Se o codigo tem um bug quando o satelite ou sonda ja ta no espaco, voce precisa contornar com o que tem. Nao da pra fazer 'git revert' em Marte.

Por causa disso, o ECSS exige que todo software espacial tenha modos de operacao degradados. Se o modulo A falha, o sistema chaveie pro modulo B. Se B tambem falha, o sistema entra em safe mode — um estado minimo que mantém a nave funcionando ate o controle de missao descobrir o que fazer.

Depois do Ariane 5, a ESA adicionou requisitos especificos sobre reuso de software. Todo modulo reutilizado precisa de uma analise de portabilidade formal que compara as condicoes operacionais do contexto original com o novo. Se os ranges de input mudaram, o modulo precisa ser re-verificado. Simples assim.

Verificacao formal: provando que o codigo esta correto

Verificacao formal e o ponto mais alto de garantia de software. Em vez de testar (que so mostra a presenca de bugs, nunca a ausencia), verificacao formal prova matematicamente que o codigo satisfaz sua especificacao pra todas as entradas possiveis.

Parece utopico? Nao e. A Amazon usa verificacao formal no AWS IAM pra provar que as politicas de acesso nao tem brechas. A Airbus usa SPARK/Ada pra verificar formalmente partes do software de voo do A380. A Microsoft usa TLA+ pra verificar protocolos distribuidos no Azure.

O custo de verificacao formal e alto — estamos falando de 10 a 50 vezes mais esforco que testes convencionais. Mas pra sistemas onde o custo de uma falha e inaceitavel, esse investimento se paga. Se o bug do Ariane 5 tivesse sido pego por verificacao formal (que provaria que o valor poderia exceder o range de int16), 370 milhoes de dolares teriam sido economizados.

Na pratica, verificacao formal e usada em modulos criticos especificos — nao no sistema inteiro. Voce verifica formalmente o modulo de autenticacao, o calculo de dosagem de radiacao, o controlador de voo. O resto usa testes convencionais. Misturar abordagens e a estrategia mais pragmatica.

O que devs de SaaS podem aprender com isso

Voce nao precisa seguir DO-178C pra sua API de agendamento. Seria insano. Mas alguns principios de software critico fazem sentido ate no projeto mais simples — e custam quase nada pra implementar.

Property-based testing merece destaque. E um meio-termo entre testes convencionais e verificacao formal. Em vez de voce definir os inputs do teste, a ferramenta gera centenas de inputs aleatorios e verifica se uma propriedade se mantém. Por exemplo: 'a funcao de calculo de preco nunca retorna valor negativo' ou 'serializar e deserializar retorna o mesmo objeto'. Ferramentas como fast-check (JS/TS), Hypothesis (Python) e QuickCheck (Haskell) fazem isso.

A mentalidade de software critico nao e sobre burocracia. E sobre pensar proporcionalmente ao risco. Seu formulario de contato pode ter bugs — e irritante, mas ninguem morre. Seu modulo de pagamento com um bug de overflow pode custar milhares de reais. Trate cada um com o nivel de cuidado proporcional ao estrago que pode causar.