Astrée Run-Time Error Analyzer

Astrée Run-Time Error Analyzer é um analisador estático que comprova a ausência de erros de execução e comportamentos concorrentes inválidos em aplicações críticas de segurança escritas ou geradas em C.

Imagens da tela

Astrée analisa programas estruturados em C com usos de memória complexas ou mesmo da alocação de memórias dinâmicas, mas sem recursão. Estes alvos incorporam aplicações embarcadas como as encontradas no transporte de terra, energia nuclear, instrumentação médica, aeronáutica e voo espacial, em um controle/comando de sincronia particular, como um controle de vôo elétrico.

Quais as propriedades de tempo de execução que são analisadas por Astrée?

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

Além disso, Astrée relata comportamentos inválidos concorrentes, violações de orientações de programação especificada pelo usuário e várias propriedades do programa relevantes para a segurança funcional.

Astrée detecta qualquer:

• Divisão por zero;
• Matriz fora dos limites de indexação;
• Manipulação errada de ponteiros e “dereferencing”;
• Acesso de leitura a variáveis não inicializadas;
• Bloqueio inconsistente;
• Chamada inválida para serviços de sistemas operacionais;
• Violação de afirmações definidas pelo usuário opcionais para provar propriedades de tempo de execução adicionais;
• Código que pode revelar-se inacessível sob quaisquer circunstâncias.

Astrée é ideal para cálculos de pontos flutuantes e lida bem com estes de forma precisa e segura. Todos os possíveis erros de arredondamento, e seus efeitos cumulativos, são tidos em conta. O mesmo é verdadeiro para valores -∞, +∞ e NaN e seus efeitos através de cálculos aritméticos e comparações.

Verificador de regras MISRA

Astrée é capaz de verificar a existência de regras de codificação MISRA, calcular métricas de código e verificar limiares métricas. O verificador de regras integrado suporta tanto MISRA 2004 quanto MISRA 2012. É altamente configurável, permitindo-lhe verificar se há regras individuais e até mesmo aspectos específicos de certas regras.