OTAWA

Features

OTAWA is mainly a framework providing facilities to handle programs in machine code and computing WCET (Worst Case Execution Time). Real-time systems are often split in tasks that, in order the system to operate in a safe way, needs to execute before deadlines. To check this deadlines, an important component is the WCET, that is, the maximum execution of a program whatever the considered inputs. To compute WCET in static and sound approach, one has to consider the running hardware and the executed program. OTAWA contributions is two-folds: (a) a set of tool to compute WCET for some hardware platforms and (b) a framework to develop new analyses for new hardware or for experimental purposes.

OTAWA provides a set of command line applications:

  • owcet to compute WCET from a script describing an hardware,
  • oRange to compute loop bounds on C code,
  • mkff to generate flow fact file ready to be filled by the user from binary code,
  • dumpcfg to output CFG (Control Flow Graph) of tasks,
  • odfa to experiment DFA (data flow analyses) on binary code,
  • opcg to dump call graph for a task,
  • odisasm to get a view of the program as understood by OTAWA.

In addition, OTAWA supports the following instruction sets:

  • ARM v5,
  • ARM v7,
  • PowerPC (including VLE mode),
  • Sparc,
  • TriCore,
  • Risc-V

OTAWA provides an extensive support for IPET (Implicit Path Enumeration Technique) for computing WCET but different approaches may be implemented. IPET requires an ILP (Integer Linear Programming) solver:

  • lp_solve v5
  • CPlex

The framework provides a layer independent of the assembly code with several program representations:

  • CFG (Control Flow Graph),
  • PCG (Program Call Graph),
  • loop identification,
  • semantic instruction,
  • context trees,
  • AST (Abstract Syntactic Tree from Heptane tool).

In the framework, the following are available:

  • loop analysis,
  • loop analysis with support of irregular loops,
  • dominance and post-dominance analysis,
  • stack analysis,
  • CLP (Circular Linear Analysis),
  • indirect branch analysis,
  • infeasible path analysis.

To run new static analyses, OTAWA provides different engines:

  • Iterative DFA (Data Flow Analysis) engine,
  • Abstract Interpretation engines.

To support the different hardware pieces, the following analyses are available:

  • extensible basic block time computation based on execution graphs,
  • several instruction powerful cache analyses based on categories approaches,
  • basic and extended data cache analyses,
  • several approaches to support branch prediction.

Through the use of different plugin, OTAWA provides full or partial support for the following hardware:

  • LPC2138 (ARM)
  • Cortex A8 (ARM)
  • MPC5554 (PowerPC)
  • Leon 2 and 3 (Sparc)
  • Cortex M4 (ARM, to come)
  • TriCore Aurix (TriCore)