Handle Incompatibilities with Automatic Stubbing

What Is Automatic Stubbing?

Automatic stubbing lets you analyze a model that contains objects that Simulink^® Design Verifier™ does not support.

When you enable the automatic stubbing option (it is enabled by default), the software considers only the interface of the unsupported objects, not their actual behavior. This technique allows the software to complete the analysis. However, the analysis may achieve only partial results if any unsupported model element affects the simulation outcome.

How Automatic Stubbing Works

If you enable automatic stubbing, when the Simulink Design Verifier analysis comes to an unsupported block, the software “stubs” that block. The analysis ignores the behavior of the block, and as a result, the block output can take any value.

Stub Trigonometric Function Block

Simulink Design Verifier does not support Trigonometric Function blocks when the Function parameter is set to acos, such as the one in the following graphic.

When stubbing this block during analysis, out_signal can take any value, with the following results.

Analysis Model	Result of Stubbing out_signal
Design error detection	If a design-error objective that depends on out_signal is proven valid, that objective is valid for all simulations. In this case, the stubbing did not affect the results of the analysis. If a design-error objective that depends on out_signal is falsified, the analysis cannot create a test case. The analysis cannot determine which input to the stubbed block produces the output that falsifies the objective.
Test case generation	If a test objective that depends on the value of out_signal is satisfied, the analysis cannot create a test case. The analysis cannot determine which input to the stubbed block produces the output that satisfies the objective. If a test objective that depends on the value of out_signal is unsatisfiable, there is no simulation that can satisfy that objective. In this case, the stubbing did not affect the results of the analysis.
Property proving	If a proof objective that depends on out_signal is proven valid, that objective is valid for all simulations. In this case, the stubbing did not affect the results of the analysis. If a proof objective that depends on out_signal is falsified, the analysis cannot create a counterexample. The analysis cannot determine which input to the stubbed block produces the output that falsifies the objective.

Stub S-Function Block Containing Function-Call Triggers

The Simulink example model sfcndemo_sfun_fcncall has an S-Function block. The S-function sfun_fcncall triggers the execution of the function-call subsystems f1 subsys1 and f2 subsys2 on the first and second elements of the first output port.

If you do not enable support for an S-function in Simulink Design Verifier and automatic stubbing is enabled, the analysis ignores the behavior of the S-function. As a result, the code that triggers the two function-call subsystems is ignored, resulting in two unsatisfiable objectives. Since the function calls are ignored, the contents of those subsystems are effectively eliminated from the analysis.

To enable support for an S-function in Simulink Design Verifier, see Support Limitations and Considerations for S-Functions and C/C++ Code

Analyze a Model Using Automatic Stubbing

This section describes a workflow for using automatic stubbing, with a simple Simulink model as an example.

• Check Model Compatibility

• Turn On Automatic Stubbing

• Review Results

• Achieve Complete Results

The following model contains a Discrete State-Space block, which is not compatible with Simulink Design Verifier.

Check Model Compatibility

From the Simulink Editor, there are two ways to check whether a model is compatible with Simulink Design Verifier: by the Simulink Design Verifier compatibility check or by running a Simulink Design Verifier analysis.

To run the Simulink Design Verifier compatibility check:

• On the Design Verifier tab, click Check Compatibility.

  

• Select the analysis that you want to perform.

  To run a Simulink Design Verifier analysis, on the Design Verifier tab, in the Mode section, select any of these options:

  • Select Design Error Detection, then click Detect Design Errors.

  • Select Test Generation, then click Generate Tests.

  • Select Property Proving, then click Prove Properties.

  The software first checks the compatibility of the model. If the model itself is incompatible, for example, if it uses a variable-step solver, the analysis cannot continue.

  If it finds incompatible elements in the model, the software analyzes the model and, by default, stubs out the incompatible elements. The Diagnostic Viewer also opens, listing the incompatibilities.

  

  Note

  For more information, see View Diagnostics.

Turn On Automatic Stubbing

Automatic stubbing is enabled by default. To change the automatic stubbing setting, in the Configuration Parameters dialog box, on the main Design Verifier pane, select Automatic stubbing of unsupported block and functions. When you run the analysis, the software tells you that stubbing is turned on and the analysis continues.

Review Results

If you run an analysis with automatic stubbing enabled, make sure to review the results. In this report, generated after a test case generation analysis, you see a table of unsupported blocks that the software encountered.

Unsupported Blocks

The generated analysis report for the example model shows that the objectives are undecided because of stubbing. The software cannot generate test cases because it does not understand the operation of the Discrete State-Space block.

Objective Undecided Due to Stubbing

Achieve Complete Results

If your analysis does not achieve complete results because of the stubbing, you can define custom block replacements to give a more precise definition of the unsupported blocks. For more information, follow the steps in Block Replacements for Unsupported Blocks.