5. QGen Model Verifier

5.1. Introduction

The QGen Model Verifier performs checks for violations of MISRA Simulink rules and verifies that the code generated from the model does not contain the errors listed below.

Warning

The QGen Model Verifier is not available by default in the QGen MATLAB user interface because it is less mature than the code generator and requires a certain experience with the QGen Code Generator in order to understand its output. To activate the QGen Model Verifier user interface, rename the file found in the QGen Installation folder share/matlab/lib/QGenVerifierReport/iqgen_verifier_mode_on.TEMPLATE to iqgen_verifier_mode_on.m and make it available in the matlab path.

  1. Possible run-time errors, including:

    • Datatype overflow (expressed as message category Overflow check)

    • Signals that might be out of range (Range Check)

    • Divide by zero errors

    • Index out of array bounds (Array index check)

  2. Dead execution paths in the control flow, detected through logic errors, for instance:

    • Conditions that might always result in the same exeuction flow

      (Test always true, Test always false, Condition predetermined)

    • Expressions that always return the same value

  3. Other functional or safety property violations, including:

    • Assertions (implemented using Simulink Assertion blocks) that might fail (Assertion)

Errors are reported in an HTML format that can be opened in the MATLAB Browser, providing direct links to the Simulink blocks where the possible errors have been found.

In some cases, backtrace information is available (see message category Precondition), allowing a better understanding of the propagation of the error throughout the model, from the block where it is detected to the top-level model.

5.1.1. Available levels of analysis

  1. Quick Check

    Performs fast, parallel analysis and reports the errors most relevant to the user. The analysis tries to avoid reporting false positives, so the findings will more likely refer to an actual problem in the model. This level is suitable for routine regular checks and can be performed on any size of the model.

  2. Deep Analysis

    Performs thorough check of the model. The analysis takes more time than the quick check. It will exhaustively detect all possible errors, however the output may include more false positives. Run this analysis when your model already passes quick check and be aware that it may take longer on large models.

    Note

    The analysis cannot be parallelized in this mode.

QGen Verifier levels

Level

Quick Check

Deep analysis

Found results

The analysis tries to find the results most relevant to the user by eliminating as many false positives as possible.

This level is exhaustive: all possible errors are reported. However, this comes at the expense of potentially many low false positive messages.

Suitable model size

No limitations on model size. The analysis is parallelized by default.

Small to medium models (generated code with less than 200K SLOC). Time of analysis may take longer on larger models. The analysis cannot be parallelized.

Use cases

Suitable for a first check of the model or for fast regular testing.

This mode may also be used in an incremental workflow where the model is verified, amended, verified again, until reaching a satisfying state.

Final analysis when few remaining changes are expected to the structure of the model and all issues in Quick Check mode have been reviewed. Use this mode to exhaustively check all possible errors that might occur in the model.

Not suitable for quick reviews because of the time required to review all false positives.

For regular testing, do not use this mode if time of analysis might be a problem.

For a more advanced understanding of the analysis levels with respect to generated source code, users may refer to level 2 (used for Quick Check) and level 4 (used for Deep Analysis) of Codepeer (Equivalent Codepeer level).

5.1.2. Categories of messages

The following categories of messages can be found in the analysis report.

Categories of messages and modeling advice

Category

Description

Action needed at model level

Test always false

The condition of the block is always false.

Check that the logic of the model is correct for this block or modify the model accordingly.

Test always true

The condition of the block is always true.

Check that the logic of the model is correct for this block or modify the model accordingly.

Condition predetermined

The condition of the block always evaluates to true or false.

Check that the logic of the model is correct for this block or modify the model accordingly.

Range check

A calculation might generate a value outside the specified range of a signal’s data type and generate an invalid value.

Ensure that input data values do not overshoot the range, e.g. using Saturation blocks.

Overflow check

A calculation might overflow the bounds of a numeric type and wrap around. The likelihood this will affect operation of the program depends on how narrow is the range of the numeric value.

You could try setting limitations to the range of the input signal data type.

Divide by zero

Second operand of a divide, mod or rem operation could be zero.

Protect the denominator input signal of the block so that it can never be zero (e.g. Input 2 of Divide Block).

Array index check

Index value could be outside the array bounds. This is also known as buffer overflow.

Ensure that the index is never out of bounds.

Assertion

This Assertion block could fail.

Ensure that the input signal to the Assertion block can never be zero.

Precondition

A call to a Subsystem or a Referenced model that might violate its preconditions. The backtrace elements are given starting from the deepest block in the model, going upwards to the root model.

Follow the advice given for each backtrace element if relevant.

Call

Means that the given precondition is associated with a call to the Block.

No action needed.

Note that originally, the messages are produced by Codepeer and apply to the source code generated by QGen Verifier, not directly to the model. The messages have been traced back to the model by QGen Verifier and the following descriptions along with advice are provided to users to help understand the messages at the model level.

More details on the original Codepeer categories can be found at http://docs.adacore.com/live/wave/codepeer/html/codepeer_ug/messages_and_annotations.html#description-of-messages

5.2. Prerequisites

Before performing model verification with QGen, it is necessary to ensure that the model is consistent and simulation can be run in Simulink with no errors.

5.3. Using qgenv

Similarly to code generation, model verification is performed by the executable qgenv which can be invoked in three methods (see next section for further details):

  1. From the Simulink GUI

    Model verification can be launched directly from within a Simulink model in the MATLAB GUI. This method is the easiest and most straightforward, however it is less flexible than the other methods in terms of the configuration options it provides.

  2. From the MATLAB Command Line

    Model verification can be launched by calling the qgen_verify function in the MATLAB Command Line. This method allows configuring the verification through arguments passed to qgen_verify.

    By default, qgen_verify will display the results in an HTML format, opening a MATLAB Browser window.

  3. From the System Command Line

    Model verification can be launched by running the qgenv executable from the system command line. This method requires a preliminary execution of the qgen_export_xmi MATLAB function to extract relevant information from the Simulink model and serialize it in multiple XMI files, one per model and one for the base workspace, as explained in Exporting the model information. Once the files are generated, qgenv no longer requires the MATLAB/Simulink environment which makes this method better suited for nightly and regression testing.

    qgenv will not display the results, but it will generate a results file in the CSV format that can be passed as input to qgen_verifier_report from MATLAB command line.

5.5. Model Verification 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.

The qgen_verify function performs the following main steps:

  1. Load the given model in Simulink

  2. Export the model information using the qgen_export_xmi function in a manner similar to Exporting the model information.

  3. Invoke the qgenv executable, which produces a CSV-formatted results file.

  4. Pass the results to the qgen_verifier_report script, which reads them and opens a MATLAB Browser window to display them in an HTML format.

As a result of step 1, Simulink itself is launched. Do not worry if you see the Simulink model being loaded upon the invocation of qgen_verify.

5.5.1. Quick Examples

Here are some quick examples on how to invoke the qgen_verify function.

Given an arbitrary model mymodel.mdl, the following invocation will output verification results for the Quick Check level in the directory qgenv_results/. The --clean argument instructs QGen to delete all contents of the output directory qgenv_results/ before analyzing the model. A file containing all model information required by QGen mymodel.xmi will be exported automatically to the default directory mymodel.mdl_qgen_xmi.

A CSV file containing the results will be generated in qgenv_results/, named mymodel.quick.qgenv. Results in the HTML format will be displayed in a MATLAB Browser window, available at qgenv_results/mymodel.quick.report.html.

>> qgen_verify ('./mymodel.mdl', 'quick', '-o', './qgenv_results', '--clean')

Let us take the example in the directory speedometer, located in the $QGEN_INSTALL/share/qgen/examples/ directory. This example requires some global variables which are defined in a separate file.

Start with loading the speedometer_def.m MATLAB file to define global variables used by the model.

>> run('./speedometer_def.m')

The following verifies the speedometer.mdl model with the Deep Analysis level and outputs results to the output directory qgenv_results/. The --clean argument instructs QGen to delete all contents of the output directory qgenv_results/ before generating code. The resulting CSV file will be generated as qgenv_results/speedometer.deep.qgenv. Results in the HTML format will be displayed in a MATLAB Browser window, available at qgenv_results/speedometer.deep.report.html.

>> qgen_verify ('./speedometer.mdl', 'deep', '--clean', '-o',
'./qgenv_results')

In the following invocation the default output directory speedometer.mdl_verified/ will be used since the -o argument was not specified. When --clean is not used and qgen_verify is run multiple times on a model, operation will be faster if the model or parts of it have not changed. The resulting CSV file will be generated as speedometer.mdl_verified/speedometer.deep.qgenv. Results in the HTML format will be displayed in a MATLAB Browser window, available at qgenv_results/speedometer.deep.report.html.

>> qgen_verify ('./speedometer.xmi', 'deep')

5.5.2. qgen_verify Arguments

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

>> qgen_verify (<mdl_path>, <level>, <exporter_options> [, <qgen_options>]);

  • mdl_path

    Name of the file containing model information, with a “.xmi” extension, optionally with path (absolute or relative). If no .xmi file is found, qgen_export_xmi will be automatically run to export model information from the mdl/slx file to XMI.

  • Level of the analysis. The accepted values are

    • quick

      Quick Check: faster but less complete verification.

    • deep

      Deep Analysis: slower but more complete verification.

Refer to Available levels of analysis for a more complete description of the analysis levels.

The exporter options switches should be provided as a single string, each value being separated by a comma.

All exporter options are documented in qgen_export_xmi Arguments.

<qgen_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. These options are identical to the options of the qgenv executable. Refer to Model Verification From the System Command Line for documentation on the generation options.

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.

  • --subsys PATH

    Verify the subsystem whose fully qualified name is PATH. For example --subsys MyModel/MySubsystem/AnotherSubsystem.

    Note

    • The selected block must be a Simulink subsystem. The option is not supported for Stateflow charts. However, the selected subsystem can contain Stateflow charts.

    • The selected Simulink subsystem can have a dedicated trigger or enable port (i.e. contain a Trigger or Enable block at the root level).

    • The selected Simulink subsystem must not have function call signals entering or leaving the subsystem’s boundary through other ports (i.e. input or output ports).

5.6. Model Verification From the System Command Line

qgenv is the core executable that performs model verification. It runs completely outside the MATLAB/Simulink environment but requires representation of the model in a set of XMI files generated from the model within MATLAB/Simulink, as explained in Exporting the model information. A file containing the results will be generated in the output folder with a CSV format.

5.6.1. Quick Examples

Given an arbitrary model mymodel.mdl and its model information file mymodel.xmi obtained with qgen_export_xmi in MATLAB, the following invocation will output verification results for the Quick Check level in the directory qgenv_results/. The --clean argument instructs QGen to delete all contents of the output directory qgenv_results/.qgenv before running the analysis.

A CSV file containing the results will be generated in qgenv_results/, named mymodel.quick.qgenv.

For example, on the speedometer.xmi file from the example in the previous section, the output will be:

>> qgenv speedometer.xmi --level quick -o ./qgenv_results

will produce the output:

[INFO] Importing XMI speedometer.xmi
[INFO] Analyzing previous generation data
[INFO] Preprocessing model speedometer
[INFO] Finished preprocessing model speedometer
[INFO] Sequencing model speedometer
[INFO] Finished sequencing model speedometer
[INFO] Generating code model speedometer
[INFO] Finished code model generation speedometer
[INFO] Printing to formal representation speedometer
[INFO] Finished formal representation printing speedometer
[INFO] Printing model debugging informations
[INFO] Finished printing model debugging informations
[INFO] Analyzing model speedometer ID= 1
[INFO] Finished model analysis speedometer ID= 1
[INFO] Generating traceability data speedometer ID= 1
[INFO] Finished traceability data generation speedometer ID= 1
[INFO] Printing model verification results speedometer ID= 1
[INFO] Finished model verification results printing speedometer ID= 1

5.6.2. qgenv Arguments

qgenv is invoked on the system command line as follows:

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

>> qgenv FILE [--level LEVEL] [switches]

  • FILE

    FILE is an .xmi file exported within MATLAB compliant with the Geneauto metamodel as available in share/qgen/plugins/geneauto/geneauto.ecore.

  • --level

    Level of the analysis. The accepted values are

    • quick

      Quick Check: faster but less complete verification.

    • deep

      Deep Analysis: slower but more complete verification.

Refer to Available levels of analysis for a more complete description of the analysis levels.

switches 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.

The accepted boolean switches are:

  • --version, -V (uppercase)

    Output version and exit.

  • --verbose, -v (lowercase)

    Verbose output.

  • --clean, -c

    Clean all results in output directory.

  • --no-misra

    Suppress warnings about violations to MISRA Simulink rules.

  • --help, -h

    Display the list of supported switches.

The following switches take a value as a separate parameter. It is assumed that the value does not start with '-' to distinguish it from other switches.

  • --output, -o DIR

    Specify the verification output directory. By default the files are placed in <modelname>.mdl_verified.

  • --lib DIR

    Provide location of external directories that contain user-defined external source files (multiple --lib arguments can be used). This is for example required when the model defines some data types with an imported scope.

  • --jobs, -j NUM

    Number of processors to use for compilation and analysis (default -j 0, use the available number of processors on the machine).

    Note

    When called with --level deep, this flag only applies to compilation of generated sources, because the analysis cannot be parallelized.

Advanced boolean switches:

  • --remove-assertions

    Remove code for assertions blocks and their inputs.

  • -k

    Do not stop at non-fatal errors.

Advanced switches that take a value parameter:

  • --arith-conf FILE

    Specify a file containing the configuration for arithmetic operations.

  • --block-conf FILE

    Specify a file containing the configuration for block libraries.

  • --unroll-threshold LIMIT

    Expand as loops when more elements than the threshold.

5.7. Reviewing Verification Results

5.7.1. Converting results to HTML from MATLAB

The QGen Model Verifier will output a file containing results in a CSV format, as explained above. These results can then be converted to a HTML format to be displayed in a MATLAB Browser window.

  • The conversion is done automatically when running qgen_verify from MATLAB command-line. The HTML report will open in the browser.

  • Manually, running the standalone script qgen_verifier_report from MATLAB command-line and passing the CSV file in argument (see qgen_verifier_report usage below).

The results can then be reviewed directly from the HTML report as explained in the following example.

5.7.2. Reviewing the results

The results of the analysis can be reviewed by users. Each result has a review status (initially “uncategorized”) and users can edit this status by clicking on the button in the “Review status” cell of the result’s table.

When editing a result status, users can add a reviewer and a comment. The status may be set to Pending, Not a bug, Intentional, False positive, Bug. After validation, the database in the results directory will be automatically updated. To display the updated review status in the report, use the “Update reviews” button.

Note

The database is separated from the generated code and from the analysis results. It will be continuously updated as long as the database folder is preserved, even if the --clean flag is used for the analysis. To reset the database, simply delete the .codepeer_<LEVEL> directory.

5.7.2.1. Quick Example

Using the speedometer.mdl model as previously explained and its exported XMI information file, a CSV results file qgenv_results/speedometer.deep.qgenv was generated with the following command from System Command Line:

>> qgenv speedometer.xmi --level deep -o ./qgenv_results --clean

These results can now be given as input to qgen_verifier_report with the command:

>> qgen_verifier_report ('speedometer.xmi_verified/speedometer.deep.qgenv','speedometer.mdl', 'quick')

Here is an example of report produced by QGen Verifier:

_images/qgenv_report.png

5.7.2.2. qgen_verifier_report Arguments

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

>> qgen_verifier_report(res_file, mdl_path, level, [format], [subsystem])

  • res_file

    Path to the CSV results file.

  • mdl_path

    Path to the .xmi file containing model information.

  • level

    Level of the analysis. The accepted values are

    • quick

      Quick Check: faster but less complete verification.

    • deep

      Deep Analysis: slower but more complete verification.

Refer to Available levels of analysis for a more complete description of the analysis levels.

  • format

    Optional. The format of the output in a string format (html (default) or text).

  • subsystem

    Optional. Specify the path to the subsystem if --subsys was used for verification.

5.7.3. Results file in CSV text format

Viewing results in HTML format is recommended over the CSV format as results are not sorted and not interactive in CSV format.

QGen Model Verifier generates a file containing the analysis results in a CSV format, described with the following fields.

  • ID

    The message identifier (for internal use).

  • Module

    The source file where the potential error was detected.

  • Line

    Line of the source file.

  • Column

    Column of the source file.

  • Category

    Category of the error.

  • History

    The status of the message (unchanged, added or removed) compared to previous analysis.

  • Ranking

    Priority of the error (Low, Medium or High).

  • Message

    Description of the error. It may be difficult to read in some cases as it relates to source code and not directly to the Simulink model, but it is given for more insight if needed. More details on its format can be found in Codepeer documentation at http://docs.adacore.com/live/wave/codepeer/html/codepeer_ug/messages_and_annotations.html#description-of-messages .

  • Block

    Path to the block in the Simulink model. For messages with a precondition category, this field is empty.

  • Backtrace

    When backtrace information is found, it is stored in the following fields. They are repeated as many times as another trace is found.

    • Backtrace Category

    • Backtrace Module

    • Backtrace Line

    • Backtrace Column

    • Backtrace Block

5.8. QGen Verifier Constraints

5.8.1. Input model constraints

In order to be analyzed by QGen Verifier, input models are required to follow the general QGen Constraints on Input Models as for code generation (e.g. the model configuration solver should be discrete fixed-step and the model should not contain unsupported blocks).

5.8.2. Specific constraints

5.8.2.1. External source code cannot be analyzed

QGen Verifier cannot analyze external source code that is referenced from the generated code. This includes:

  • custom data types defined in external modules

  • variables and constants imported from external modules through Simulink Parameters or Simulink Signals (using for example the “ImportedExtern” storage class, see Simulink Coder(TM) Parameters)

  • external C or Ada code that is referenced by the model through a S-Function

See also Integrating external code for more information about the use of external code with QGen.

For example, if an S-Function links to a function that contains a violation, such as a potential division by zero, it will not be detected by the analysis.

5.9. Troubleshooting

5.9.1. General notes

There are several different workflows for using the tool. E.g. launching from the Simulink GUI, the qgen_verify script or explicitly from the system command line. The error messages may vary slightly depending on the chosen workflow.

5.9.1.1. Errors at model export or during code generation

QGen Verifier may fail in its early steps, at model export to XMI or during code generation, in any of the steps before reaching the step “Analyzing model speedometer” in the following example:

[INFO] Importing XMI speedometer.xmi
[INFO] Preprocessing model speedometer
[INFO] Finished preprocessing model speedometer
[INFO] Sequencing model speedometer
[INFO] Finished sequencing model speedometer
[INFO] Generating code model speedometer
[INFO] Finished code model generation speedometer
[INFO] Printing to formal representation speedometer
[INFO] Finished formal representation printing speedometer
[INFO] Printing model debugging informations
[INFO] Finished printing model debugging informations

In such cases, it may be helpful to:

  1. use the -v or --verbose option to get more information.

  2. try using the QGen Compatibility Checker to identify possibly unsupported blocks or model settings. Try fixing the reported warnings and errors.

  3. refer to Appendix A: Errors and warnings to identify the error and to QGen Constraints on Input Models to understand the QGen constraints associated to Simulink blocks, Stateflow charts and the supported set of features.

  4. contact us if blocked (see Reporting Suggestions and Bugs).

5.9.1.2. Errors during model analysis

If QGen Verifier could complete the model analysis but failed before finishing printing the verification results, in any of the following steps:

...
[INFO] Analyzing model speedometer ID= 1
[INFO] Finished model analysis speedometer ID= 1
[INFO] Generating traceability data speedometer ID= 1
[INFO] Finished traceability data generation speedometer ID= 1
[INFO] Printing model verification results speedometer ID= 1
[INFO] Finished model verification results printing speedometer ID= 1

It means that the static analysis may have failed.

  1. use the -v or --verbose option to get more information.

  2. if the analysis is not a first run on the model, but an iteration on an analysis that was pre-existing, there may be a conflict with the analysis database (which may be found at <output_folder>/.codepeer_<level>). This is not supposed to happen as the database should be robust to incremental runs. However, if the model has been substantially modified and there are any doubts regarding that database, you may try to backup the database folder to a safe directory and run the analysis again. This will produce a new database. Be aware that all existing reviews of the messages for the model will be removed, unless the original database is restored.

  3. contact us if blocked (see Reporting Suggestions and Bugs).

5.9.1.3. Issues when reviewing the results

If QGen Verifier successfully completed but there are issues when generating the HTML report or to edit reviews:

  1. when setting a review, if the error reports that the database cannot be reached, then it may be that codepeer_bridge (the tool to query Codepeer’s database) is not found. The command iqgen_codepeer_bridge from the MATLAB command-line should return:

Usage: codepeer_bridge <command_file>

If it does not, check that QGen is properly installed in MATLAB.

  1. contact us if blocked (see Reporting Suggestions and Bugs).