A matemática além das formúlas? Testando com linguagem formal? · KitsuneSemCalda

Eu sei, fiz um post rant gigante sobre a importância da matemática e estamos aqui de novo para falar dessa maravilhosa linguagem.

Hoje sobre aspectos de testes onde é necessário total controle sobre o software produzido em "voos espaciais ou aéreos".

Utilizando obviamente linguagem formal.

E que caralhos é linguagem formal?

Como dito em comentário no post anterior feito por amigo @maniero.

A matemática possui diversos tipos de aritméticas, formas de pensar, provar e se descrever.

Eu mesmo disse que a própria matemática é comprovadamente incompleta segundo o teorema da incompletude de Gödel.

O pensamento matemático é importante para muitas coisas e em vez de descrevermos tudo em fórmulas podemos usar a linguagem formal.

A linguagem formal veio através do estudo de modelos matemáticos que especificam o reconhecimento de linguagens (no sentido mais amplo).

Fica fácil ver onde isso é aplicado na computação:

NLP (obviamente).
Aspectos da computação (decibilidade, computabilidade, complexidade computacional).
Criação de novas linguagens de (programação, configuração, marcação ...).

Inclusive o modelo matemático de uma máquina de Turing é escrita em linguagem formal da seguinte forma:

M = (Q, \Sigma, \Gamma, \delta, q_0, q_{\text{aceite}}, q_{\text{rejeição}})

Onde:

$Q$ é o conjunto de estados,
$\Sigma$ é o alfabeto de entrada,
$\Gamma$ é o alfabeto da fita (onde $\Sigma \subseteq \Gamma$ ),
$\delta: Q \times \Gamma \to Q \times \Gamma \times \{L, R\}$ é a função de transição,
$q_0 \in Q$ é o estado inicial,
$q_{\text{aceite}} \in Q$ é o estado de aceitação,
$q_{\text{rejeição}} \in Q$ é o estado de rejeição.

Ok, pode parecer meio complexo, mas essa é toda definição de uma máquina de Turing escrita totalmente por Alan Turing.

Deixando um pequeno disclaimer, Turing não inventou o computador moderno, apenas a definição formal (mostrada acima de uma máquina de Turing).

E essa é uma das formas de se usar a matemática "descrever autômatos" que inclusive é o nome de uma matéria do curso de ciência da computação basicamente o inventor da arquitetura moderna de computadores foi John Von Neumann

Introduzindo o SEL4

Sabia que o kernel usado em aviões e alguns sistemas de alta urgência não usa Linux? Pois é, eu fiquei meio surpreso quando descobri isso, mas eu já tinha ciência de que Linux apesar de ser muito usado, não é unânime.

Sony e Nintendo preferem usar o BSD como base de código para seus consoles.
Netflix usa o BSD como roteador de rede principal
Apple usa uma parte do código BSD e uma parte do código Mach para seu kernel XNU.

Agora um que provavelmente vocês não conhecem, não é base Linux, nem XNU e nem BSD é o SEL4.

SEL4 é um micro-kernel (Andrew Taunenbaum deu 101 palmas aqui) implementado como POSIX e descrito como um dos kerneis mais confiáveis que temos atualmente.

Porque caralhos o SEL4 é um Micro-Kernel

Que Micro-kerneis são lindos teoricamente e horríveis fisicamente já foi discutido em um maravilhoso debate Torvalds vs Taunenbaum.

Mas nada existe sem um porquê?

E sendo o L4 uma família de microkerneis de 3ª geração já da para praticamente entender o que aconteceu.

Tentando ser arrojados demais na implementação do Mach.

Muita coisa ficou bloated. Então eles fizeram o óbvio e removeram o over-enginerring.

E para garantir que o kernel seja seguro em qualquer caso eles realizam a verificação formal das funções.

Obviamente, funções da linguagem podem ser reduzidas a funções matemáticas $$F(x) = fórmula$

E realizasse verificações matemáticas para garantir que o que foi escrito funcione sobre quaisquer situações.

Aqui entrando na lógica matemática para realizar o teste de premissas.

Exemplificando a verificação formal

Para termos uma verificação formal, começamos com a especificação formal para descrever de forma rigorosa o que o código deve fazer.

Sendo rigorosa porque matemática não aceita lidar com ambiguidades, tudo deve ser exato.

Depois disso criamos uma representação formal do código, ou seja, onde as partes críticas são reduzidas a suas formas matemáticas básicas.

E por fim, uma validação de teoremas verifica se a representação formal satisfaz a especificação formal.

E para linguagem C, temos algumas ferramentas para isso como o Coq, SPIN e TLA+.

Exemplo prático

Imagine um sistema que controla freios ABS em carros onde erro nesse software pode ser fatal.

Vamos aplicar a verificação formal:

Especificação Formal: Você define, matematicamente, o comportamento esperado. Por exemplo:

"A distância de frenagem não pode ultrapassar X metros em condições normais."
"Se uma roda travar, o sistema deve reduzir a pressão sobre ela dentro de Y milissegundos."

Modelagem: Pegamos o código responsável pelo controle dos freios e o representamos matematicamente, como funções ou diagramas de estados. Exemplo:

Entrada: Velocidade atual, pressão do freio.
Saída: Nível de pressão ajustado.

Prova Formal: Um sistema automatizado pega essa modelagem e verifica, por lógica matemática, se o software cumpre as condições definidas SEMPRE — independente da entrada ou do cenário.

Comparando testes tradicionais e verificação formal

Testes tradicionais:

Você roda o software em um conjunto de cenários e analisa os resultados.

Desvantagem: Você não cobre todos os casos possíveis. Sempre há aquele cenário improvável que vai dar problema (e você só descobre depois que o bug já causou estrago).

Verificação formal:

Você prova que TODOS os casos possíveis estão cobertos.

Desvantagem: Mais complicado de fazer, e exige mais esforço inicial.

Conclusão

Se após ler isso, você quer implementar verificação formal do seu projetinho uni-esquina ou seu sistema web.

É a hora de pegar minha mão e dar um tapa na sua cara.

Eu, mano @maniero, e muitos outros já falamos análise com cuidado e cautela as ferramentas que você usa.

Verificação formal foi feito para sistemas críticos.

Coisas que pessoas com anos de estudos em todas as matérias de uma faculdade deveria codificar.

SISTEMAS CRÍTICOS:

Aviões: Sistemas de controle de voo como o usado em caças militares e aviões comerciais passam por verificação formal para garantir que nenhuma falha acontece em situações extremas.
Blockchain: Contratos inteligentes em plataformas como a Ethereum usam verificação formal para evitar problemas como roubo de fundos.
Medicina: Máquinas como ventiladores pulmonares usam verificação formal para evitar erros fatais.