4. QGen Model Verifier

The QGen Model Verifier performs checks for MISRA violations, and verifies that the code generated for the model does not suffer from one of the following possible run-time issues:

  1. Possible run-time errors, including:
    1. Integer overflow
    2. Signal out of range
    3. Division by zero
  2. Logic errors, including:
    1. Conditions that are always true, or always false
    2. Expressions that always return the same value
  3. Other functional or safety property violations, including:
    1. Simulink Assertion blocks that might fail

4.1. Using qgenv

Similarly to code generation, model verification is performed by the executable qgenv which can be invoked in three methods:

  1. From the Simulink GUI
  2. From the MATLAB Command Line
  3. From the System Command Line

4.3. From the MATLAB Command Line

QGen model verification can be invoked from the MATLAB command line using the qgen_verify function. This requires QGen to be correctly setup in MATLAB following the instructions in Setting up QGen in MATLAB.

qgen_verify has two required inputs and a number of optional parameters:

qgen_verify (<mdl_path>, <mode> [, <options>]);

  • mdl_path

    Name of the mdl or slx file optionally with path (absolute or relative).

  • mode

    Verification mode. The accepted values are

    • --bug-finder

      Executes a faster but less complete verification.

    • --proof

      Executes a slower but more complete verification.

<options> are all string values. Each option is either a single boolean switch or a switch followed by a value. Options can be passed in an arbitrary order.

Note

Several options correspond to identical or similar options of the qgenv executable. As a result, more details on options will be provided in From the System Command Line.

Note

Options can be passed either as function arguments, or as a cell array of length 1 where the value of the first element is also a cell array containing the list of options.

The accepted boolean switches are:

  • --wmisra

    Treat violations to MISRA Simulink as warnings.

  • --no-misra

    Allow violations to MISRA Simulink.

  • --export-ws, -w

    Export workspace contents to m-file and ignore any MATLAB files passed in the function input.

  • -v

    Print verbose output when exporting the decoration file

  • --clean, -c

    Instructs QGen to delete all the content of the output directory before starting the code generation.

  • --incremental, -i

    Instructs QGen to leave the content of the output directory as is. Generated files will overwrite existing files with the same name, but other existing files will remain untouched.

Switch-value pairs shall be passed as two arguments. First is the key and the second is value. It is assumed that the value does not start with '-' to distinguish it from other switches

  • --subsys

    Generate code for the subsystem identified by the name in argument (the name is a /-separated path of subsystem names starting from the model root)

  • --output, -o

    Specify the code generation target directory. By default the files are placed in <modelname>_generated.

  • --matlab, -m

    Provide a MATLAB file containing the constant, Bus and Signal definitions.

Example command:

qgen_verify ('test.mdl', '--proof', '-m', 'test_def.m')

4.4. From the System Command Line

qgenv is invoked on the system command line as follows:

qgenv FILE [switches]

The arguments of the qgenv executable are:

  • FILE

    An slx or mdl Simulink model.

  • --bug-finder

    Executes qgenv in bug-finding mode, which perform a faster but less complete verification using Codepeer. This switch cannot be passed simultaneously with the --proof switch.

  • --proof

    Formally verify the model. This implies a slower but more complete verification. Cannot be passed together with --bug-finder switch.

  • --version, -V

    Output version and exit.

  • --from-simulink

    Display error messages as hyperlinks in the Simulink console.

  • --help, -h

    Display the list of supported switches.

  • --matlab, -m FILE

    Provide MATLAB file containing the definitions of variables used by the Simulink model.

  • --wmisra

    Treat violations to MISRA Simulink as warnings.

  • --no-misra

    Allow violations to MISRA Simulink.

  • --subsys PATH

    Provide the path to the subsystem to verify.

  • --typing, -t FILE

    Provide the decoration file.

  • --lib, -b FILE

    Specifies directories where library models can be found. The switch can be used multiple times to specify multiple directories.

    Note

    The --lib switch is required only in case the relative location of the libraries is different than at the time of generating the decoration file. The new location given with the --lib switch will override the original location which is stored in the decoration file.