TAnOTaTU -- 9h
As fontes descrevem uma vasta gama de linguagens e ferramentas projetadas para aplicar o rigor matemático em
diferentes etapas do desenvolvimento de sistemas, desde a especificação inicial até a verificação do código
final.

### **Linguagens de Especificação Formal**
As linguagens de especificação são fundamentais para criar descrições precisas e sem ambiguidades do
comportamento pretendido de um sistema [1, 2]. Entre as principais mencionadas estão:

* **Z notation e B-Method:** Frequentemente utilizadas para software sequencial [3, 4]. O B-Method, em
particular, é utilizado com a ferramenta **Atelier B** para desenvolver sistemas críticos de segurança em metrôs
ao redor do mundo [5, 6].
* **Alloy:** Uma notação de modelagem de objetos focada em uma abordagem "lightweight" (leve), utilizada para
explorar designs e verificar propriedades estruturais [4, 7, 8].
* **TLA+:** Uma linguagem de especificação amplamente utilizada para modelar e verificar sistemas complexos e
concorrentes [4].
* **SPARK Ada:** Um subconjunto da linguagem Ada que utiliza anotações formais para permitir a verificação de
código em sistemas de alta criticidade [4, 9, 10].
* **JML (Java Modeling Language):** Utilizada para especificar formalmente o comportamento de programas Java
através de contratos de código [3, 4, 11].
* **VDM (Vienna Development Method):** Inclui linguagens de especificação como VDM-SL e VDM++, focadas na
modelagem rigorosa de sistemas [4, 8].
* **Linguagens para Concorrência:** Incluem **Petri nets**, **Álgebra de Processos** (como **CSP**, **LOTOS** e
**π-calculus**) e máquinas de estados finitos [4, 12].
* **Linguagens de Modelagem de Arquitetura:** Como **AADL** (Architecture Analysis & Design Language) e
**SysML**, que funcionam como plantas para definir a estrutura e o comportamento de sistemas complexos [13-16].

### **Ferramentas de Verificação e Análise**
As ferramentas automatizam o processo de provar que um sistema adere à sua especificação matemática [2]. Elas
são categorizadas principalmente em:

* **Model Checkers (Verificadores de Modelos):** Realizam buscas exaustivas em todos os estados possíveis de um
sistema para garantir que propriedades específicas sejam mantidas [17]. Exemplos incluem **SPIN**, **UPPAAL**,
**ESBMC**, **FizzBee**, **PAT** e **CBMC** (específico para C) [16, 18, 19].
* **Provadores de Teoremas (Theorem Provers):** Ferramentas que auxiliam na construção de provas lógicas formais
[17]. O **ACL2** é utilizado por empresas como IBM e Intel para verificar hardware [20, 21]. Outros exemplos
incluem **PVS** (Prototype Verification System) e **HOL Light** [21, 22]. Ferramentas como **Coq** e
**Isabelle** também são mencionadas como poderosas, embora exijam alto treinamento [23].
* **Análise de Software e Código:**
* **SAW (Software Analysis Workbench):** Utilizada para construir modelos semânticos de programas e verificar a
correção de algoritmos criptográficos [24-26].
* **Frama-C:** Uma plataforma para análise estática e verificação de programas em C baseada em contratos [9, 16,
23].
* **Logika/Sireum:** Uma estrutura de verificação para as linguagens Scala e Slang [9, 27, 28].
* **C2Rust:** Ferramenta que traduz módulos C para Rust, visando melhorar a segurança de memória em sistemas
legados [24, 29].
* **Solvers:** Ferramentas como **SAT solvers** e **SMT solvers** são componentes essenciais que resolvem
problemas de lógica booleana e satisfatibilidade, servindo de motor para muitas das outras ferramentas de
verificação citadas [18, 30, 31].
reply