Astrée
Ferramenta de análise estática de código fonte:
Deteção de erros de tempo de execução e de simultaneidade
Cinco razões para escolher a Astrée
Astrée é uma ferramenta de topo de gama, baseada em métodos formais, que garante que, quando não detecta erros em tempo de execução, a aplicação não tem efetivamente erros em tempo de execução.
Até à data, existem apenas duas ferramentas no mercado, baseadas em métodos formais, que podem fornecer esta garantia.
1. funciona
Funciona para aplicações escritas em linguagem C.
2. Detetar
- Erros de simultaneidade no sistema operativo OSEK e no perfil ARINC 653.
- Erros de divisão por zero.
- Erros de acesso à matriz fora do intervalo.
- Manipulações incorrectas de ponteiros.
- Estouro de variáveis inteiras e de ponto flutuante.
- Erros de arredondamento em cálculos de vírgula flutuante.
- Acessos a variáveis não inicializadas.
- Acesso simultâneo problemático a variáveis partilhadas por vários processos.
- Erros de inconsistência de bloqueio de variável.
3. Permite
- Permite o diagnóstico de asserções definidas pelo utilizador para testar propriedades adicionais em tempo de execução.
- Permite testar que partes do código não são executáveis em nenhuma circunstância(deteção de código morto).
4. Verificar
Verificar o código-fonte em relação às seguintes normas de codificação de software:
- MISRA C (2004 e 2012, incluindo a alteração 1)
- Linguagem C99 (Anexo J da ISO/IEC 9899:1999)
- CWE (exatidão do CCR, CWE mais abstrato e CWE mais específico)
- SEI CERT C
- ISO/IEC TS 17961:2012
5. Para além disso...
- Tem um IDE e uma interface de linha de comandos, permitindo a execução em lote para facilitar os testes de regressão.
- Tem integrações com Jenkins, SCADE, TargetLink (dSPACE), SymtaVision e RT-Druid.
- Dispõe de um pacote decertificação para DO-178, ISO 26262, EN-50128 e FDA.
