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.
The license for the WCET tools can be found in the
LICENCE.txt file in the repository.
Installation instructions can be found in the README.md files in graph-refine and graph-refine/graph_to_graph respectively.