Ferramentas de análise estática de código binário
Cálculo do tempo de execução no pior dos casos (WCET)
Ferramenta: aiT
Para que serve?
1.
Calcula limites de WCET muito precisos e pode ser utilizado para gerar provas de certificação deste objetivo.
2.
Dispõe de um pacote de qualificação, conforme exigido pelas normas de segurança funcional.
3.
Determina o caminho de execução com o pior tempo de execução e tem em conta aspectos de baixo nível, como o pipeline e a cache do processador específico utilizado. Para o efeito, utiliza o método formal"Interpretação abstrata" juntamente com modelos formais de pipeline e de cache.
4.
Requer apenas o código de objeto executável para realizar a análise, embora, se for fornecido código fonte, este seja incluído na saída juntamente com o código de montagem gerado.
5.
Calcula o tempo de execução de cada um dos caminhos de um programa ou tarefa e marca a vermelho o caminho crítico correspondente ao WCET.
6.
Utiliza ficheiros de anotação relativos à arquitetura do processador, frequência de relógio e outros parâmetros necessários para o cálculo do tempo de execução.
7.
Permite comparar graficamente o resultado de diferentes execuções da ferramenta para monitorizar a evolução do WCET.
8.
Pode ser utilizado com geradores de código de ferramentas de modelação e ferramentas de planeamento ao nível do sistema através de uma API baseada em XML.
9.
No entanto, os actuais processadores multi-core têm um nível de complexidade que dificulta a análise dos efeitos do pipeline e da cache em ambientes de execução complexos em que diferentes núcleos interagem entre si. A interferência entre núcleos não pode ser formalmente modelada no AiT.
10.
Para processadores multi-core, é necessária a ferramenta TimeWeaver.
Famílias de processadores e compiladores suportados
- Compilador ARM
- Compilador GCC
- Diab C ou Ada
- Green Hills C/C++ ou Ada
- IAR
- Keil ARM
- HighTec LLVM/Clang
- Atribuição de tarefas
- Texas Instruments
- CompCert (INRIA, AbsInt)
- Diab C
- Green Hills C/C
- Compilador GCC
- Diab C
- Green Hills C/C++ ou Ada
- HighTec GCC
- Atribuição de tarefas
- Compilador Code Warrior
- Compilador GCC
- GNAT Pro C++ ou Ada
- Diab C ou Ada
- Green Hills C/C++ ou Ada
- HighTec GCC
- Keil ARM
- CompCert (INRIA, AbsInt)
- Compilador GCC
- GNAT Pro C++ ou Ada
- Diab C ou Ada
- Green Hills C/C++ ou Ada
- HighTec GCC
- Keil ARM
- CompCert (INRIA, AbsInt)
Outros processadores
- ERC32
- Leon2, Leon3
- Am486, IntelDX4
- i386DX
- C16x, ST10
- HCS 12
- C28X
- C33
- M68020, MCF5307, M68020, MCF5307
