Hybrid Program Analyser

This guide describes the installation process and tool usage of the hybrid program analyser. The hybrid program analyser (HPA) is part of the COde Behaviour fRAmework (COBRA). The HPA tool is designed to perform worst-case resource analysis in order to determine the code behaviour on a specific target. Therefore, a hybrid methodology is used to determine the worst-case resource consumption. This hybrid approach combines two methodologies: static analysis and measurement based analysis. The COBRA-HPA elaborates on this principle and implements the two-layered hybrid analysis model. In the first step, the framework splits the source code of a set of tasks into so-called basic blocks (Block Generator). In the second step, each block is deployed to the targeted hardware and the appropriate measurements are conducted (Profiling Generator, Profiling Assistant). The final step will combine and/or analyse all the results to achieve a sound approximation of the worst-case resource consumption or conduct further analysis (Export Tools). A schematic overview of the COBRA-HPA framework is presented in the figure below.
This toolchain is currently under development and does not contain its full functionality yet.

Prerequisites

In order to run the hybrid program analyser tools, the following software packages are required.

Minimal requirements

Java JRE x64 11 or higher

Additional packages

UPPAAL 4.0 or higher (only required for exporting to UPPAAL)

Project Wizard

The HPA toolchain perform its operation based on a Project Configuration File that will be used through the entire chain. This file contains the user-defined parameters characterizing how the input source files need to be processed. The configuration files used in the toolchain are all formatted in XML-style. A template can be found here. The Project Wizard is a non-mandatory tool designed to give the operator an user-friendly interface to define all parameters. Subsequently, the tool generates a configuration file conform to the requirements of the framework.
This tool is currently in development... Available soon!

Block Generator

The Block Generator can be downloaded from this location. This tool only requires the corresponding JAR file and the minimal prerequisites. In order to generate a block model out of the source code, a project folder needs to be prepared first. This can be done with the Project Wizard or manually with a template project file (download).

Creating project folder manually

Create an empty folder;
Copy all source files into a source folder (e.g. './sources/');
Create a project configuration file. An example with instructions can be found here.

The project folder should now have a similar structure as the example below:

                                        ProjectFolder
├─ project.xml
└─ sources
   ├─ mySource1.c
   └─ mySource2.c

The corresponding project configuration file (project.xml) for the example above is shown below:

                                        <project>
    <name>myProject</name>
    <version>1.0</version>
    <grammar>C</grammar>
    <sources>
        <source id="01">
            <location>./sources/mySource1.c</location>
        </source>
        <source id="02">
            <location>./sources/mySource2.c</location>
        </source>
    </sources>
    <config>
    </config>
</project>

Run the Block Generator
The following commands give a brief summary how the tool can be used to generate a block model:

                                        Generic usage:
java -jar BlockGenerator.jar [options] config_file

Generate block model according to the given config file:
java -jar BlockGenerator.jar "./ProjectFolder/project.xml"

To get a list of all possible parameters and options using the argument '--help':
java -jar BlockGenerator.jar --help

Output
After block generation has finished, a new file 'model.xml' is created in the project folder. This file contains a data representation of the generated block model(s). The block model is represented as a tree structure which is built out of blocks. Each block initially contains one instruction or statement of the source code. The blocks are arranged from left to right to their sequential order in the code. Instructions that reside inside a statement body are added as child 'blocks' to the parent block. The block model exists out of seven types of blocks (extended with more specific subtypes) in which the blocks are categorized according to their instruction type. These block types are shown in the following class diagram:

All COBRA-HPA tools are compatible with the generated model files. The analysis flow is made easy and adaptable to the user needs by using only one project folder for all HPA tools.

Example
When using the '--show-graph' option, a graphical representation is displayed after generating the block model. A code example with its resulting graph is shown below:

                                        int main(int argc, const char* argv) {
    int var1, var2;
    int array[10];

    if(argc == 1)
        var2 = atoi(argv);
    else
        var2 = 1;

    for(var1 = 0; var1 < 10; var1++) {
        array[var1] = var1 * var2;

        if(array[var1] > 100)
            break;
    }

    return 0;
}

Profiling Generator

In development... Available soon!

Profiling Assistant

In development... Available soon!

Export Toolbox

The Export Toolbox is a collection of tools to assist the user in formatting and exporting models to other applications.

UPPAAL Exporter

UPPAAL is a model-checker toolbox developed by Uppsala University and Aalborg University. It is designed to verify systems which can be represented as a network of timed automata. The UPPAAL Exporter tool allows the user to transform a generated hybrid block model into a timed automaton representation in a project file compatible with the UPPAAL model-checker tool. The export tool can be downloaded from this location.

Run the UPPAAL Exporter
The following commands give a brief summary how the tool can be used to generate a UPPAAL model:

                                        Generic usage:
java -jar UPPAALExporter.jar [options] project_location

Generate UPPAAL model according to the given project folder:
java -jar UPPAALExporter.jar "./ProjectFolder/"

To get a list of all possible parameters and options using the argument '--help':
java -jar UPPAALExporter.jar --help

Output
After model transformation has finished, a new file 'uppaal.xml' is created in the project folder. This XML file complies to the project file syntax of the UPPAAL model-checker tool. All block models that are present in the project folder will be combined into one UPPAAL project file. The figure below shows an example project file opened in UPPAAL v4.0.14 which was generated with the UPPAAL Exporter tool.

Project file in the UPPAAL model-checker