Worst-case execution time computation tools

Based on our translation validation work, our graph-to-graph toolchain is capable of performing control flow graph extraction, loop bound computation and infeasible path eliminations. It uses a modified version of the Chronos 4.2 WCET analyzer for microarchitectural analyses. The default modelled hardware is the ARM1136 i.MX31 processor on the KZM evaluation board.

This software was developed as part of our research in mixed-criticality real-time systems, and has been used to compute execution time bounds for seL4.

Limitations

• Only a subset of instructions of the ARMv6 instruction set are supported. In particular, floating point, VFP, NEON, division and 64-bit multiplication instructions are not supported.
• The branch predictor is modelled as disabled.
• The L2 cache is modelled as disabled (although it can be enabled).
• The tools are unable to analyse binaries containing function pointers, recursive functions and unbounded loops.
• The toolset can only be used on C code that falls within our verification subset of C, as required by the c-parser. 

License

The license for the WCET tools can be found in the LICENCE.txt file in the repository.

Download

• graph-refine on GitHub

Installation instructions can be found in the README.md files in graph-refine and graph-refine/graph_to_graph respectively.