Main Content

Extend Test Cases for Model with Temporal Logic

Create Starting Test Case

This example uses the sldvdemo_sbr_extend_design model. This model includes a Stateflow® chart SBR that uses temporal logic. The transition from the KEY_OFF state to the KEY_ON state occurs after the Stateflow chart has been simulated 500 times. To test this transition requires a test case with 500 time steps.

In this example, you create a test case that forces the transition to KEY_ON by setting the KEY input to 1 for the duration of the test case. You simulate the model using this test case, satisfying the objectives for the KEY_OFF/KEY_ON transition. Then you analyze the model, ignoring the objectives already satisfied by the test case you create.

  1. Open the example model:

    openExample('sldv/DefiningExtendingExistingTestsCasesExample',...
'supportingFile','sldvdemo_sbr_extend_design');

  2. Open the SBR Stateflow chart to see the KEY_OFF/KEY_ON transition.

    SBR Stateflow chart showing KEY_OFF and KEY_ON.

  3. Create a model reference harness model:

    [~, harnessModelFilePath] = ...
    sldvmakeharness('sldvdemo_sbr_extend_design',[],[],true);

    The harness model, sldvdemo_sbr_extend_design_harness, includes:

    • A Model block named Test Unit that references the original model, sldvdemo_sbr_extend_design.

      Model block named Test Unit with Inputs as input and SeatBeltIcon as output.

    • A Signal Editor block named Inputs that contains the test-case inputs to the model referenced in the Model block.

      Signal Editor block.

      Initially, the Signal Editor block contains only the default test case, with all three inputs set to 0.

    • A DocBlock block named Test Case Explanation that documents the test case.

      A DocBlock named Test Case Explanation.

      Initially, the Test Case Explanation block does not have any content for the default test case.

  4. sldvmakeharness returns the path to the harness model file in harnessModelFilePath. Extract the name of the harness model file into harnessModel, for later use:

    [~, harnessModel] = fileparts(harnessModelFilePath);

In order to analyze the KEY_OFF to KEY_ON state transition, create a test case that makes the transition to the KEY_ON state in 500 time steps in Signal Editor block. Close the Signal Editor block.

Log Starting Test Case

The next step is to log the starting test case that you created. You can then specify that Simulink® Design Verifier™ ignore the objectives satisfied by that test case when performing an analysis.

The sldvlogsignals function records the test case data in a MAT-file that contains an sldvData structure. This structure stores all the data that the software gathers and produces during the analysis.

To log the starting test cases:

  1. Save the name of the Model block in the harness model that references the sldvdemo_sbr_extend_design model:

    [~, modelBlock] = find_mdlrefs(harnessModel, false);

  2. Simulate the model referenced by the Model block using the new test case, and log the input signals in the workspace variable loggeddata:

    loggeddata = sldvlogsignals(modelBlock{1});

  3. Save the logged data in a MAT-file named existingtestcase.mat:

    save('existingtestcase.mat', 'loggeddata');

    You will specify this file when you analyze the sldvdemo_sbr_extend_design model.

Extend Existing Test Cases

You can now analyze the sldvdemo_sbr_extend_design model and specify that the analysis extend the test cases already satisfied. The analysis uses the existing test-case data as a starting point, and does not try to generate test cases for the KEY_OFF to KEY_ON transition in the SBR Stateflow chart.

Specify the starting test case and analyze the model:

  1. Open the model.

    open_system('sldvdemo_sbr_extend_design');

  2. On the Design Verifier tab, click Test Generation Settings.

  3. In the Configuration Parameters dialog box, on the Test Generation pane, under Existing test cases, select Extend existing test cases.

  4. In the Data file field, enter the name of the MAT-file that contains the logged data:

    existingtestcase.mat

  5. Clear Ignore objectives satisfied by existing test cases.

    When you clear this option, the software includes the starting test case in the final test suite. You will see that the complete test suite achieves 100% model coverage.

  6. To close the Configuration Parameters dialog box, click OK.

  7. Save the sldvdemo_sbr_extend_design model on the MATLAB® path with the name sldvdemo_sbr_extend_design_test.

  8. Click Generate Tests.

    The log window first lists the objectives that the starting test case satisfied.

    Results analysis window for test case generation.

    The log window then lists the objectives generated beyond the starting test case.

Verify Analysis Results

To make sure that this analysis creates a complete test suite, generate the harness model so you can simulate the model with the generated test cases:

  1. On the Design Verifier tab, in the Review Results section, click Create Test Harness Model.

  2. In the harness model sldvdemo_sbr_extend_design_test_harness, open the Signal Editor block named Inputs.

  3. To simulate the model using all the test cases, click the Run all and produce coverage button .

    When the simulation is complete, the model coverage report is displayed.

  4. View the coverage information for the sldvdemo_sbr_extend_design_test model to see that the complete test suite achieves 100% coverage.

    Coverage information for the model showing 100% coverage.

Related Examples

More About