Astrée

Astrée

Astrée é um analisador de código estático que prova a ausência de erros de tempo de execução e comportamento concorrente inválido em software crítico de segurança escrito ou gerado em C.

Astrée é voltado principalmente para aplicações embarcadas, como encontradas na aeronáutica, no transporte terrestre, na instrumentação médica, na energia nuclear e no voo espacial. No entanto, também pode ser usado para analisar qualquer programa C estruturado, manuscrito ou gerado, com usos complexos de memória, alocação de memória dinâmica e recursão.

Quais propriedades do software Astrée?

Astrée analisa se a linguagem de programação C é usada corretamente e se pode haver erros de tempo de execução durante qualquer execução em qualquer ambiente. Isso cobre qualquer uso de C que, de acordo com o padrão C99, tenha comportamento indefinido ou viole aspectos específicos de hardware.

Além disso, a Astrée reporta comportamento concorrente inválido, violações das diretrizes de programação especificadas pelo usuário e várias propriedades do programa relevantes para a segurança funcional.

Astrée detecta

• Divisão por zero,
• Indexação de matriz fora dos limites,
• Manipulação incorreta de ponteiro e de referenciamento (ponteiros NULL, não inicializados e pendentes),
• Excesso aritmético de inteiros e de ponto flutuante,
• Acesso de leitura a variáveis não inicializadas,
• Corridas de dados (acessos simultâneos de leitura / gravação ou gravação / gravação por dois encadeamentos para o mesmo local de memória sem bloqueio de mutex adequado),
• Bloqueio inconsistente (problemas de bloqueio / desbloqueio),
• Chamadas inválidas para serviços do sistema operacional (por exemplo, chamadas do OSEK para Terminate Taskuma tarefa com recursos não liberados),
• Violação de asserções definidas pelo usuário opcionais para comprovar propriedades de tempo de execução adicionais (semelhante a assert diagnostics),
• Código pode provar ser inacessível em qualquer circunstância.

Adapte-o às suas próprias necessidades

Astrée oferece poderosos mecanismos de anotação para fornecer conhecimento externo e aperfeiçoar a precisão da análise para loops individuais ou estruturas de dados. Mensagens detalhadas e uma GUI intuitiva que guia você até a causa exata de cada erro de tempo de execução potencial. Os erros reais podem ser corrigidos e no caso de um alarme falso, o analisador pode ser ajustado para evitá-lo. Isso permite análises com poucos ou até zero falsos alarmes.

Requisitos de sistema

Windows: Windows 7 de 64 bits SP1 ou mais recente

Linux: CentOS / RHEL 6 de 64 bits ou compatível

4 GB de RAM (16 GB recomendados)

4 GB de espaço em disco