User manual MATLAB SIMULINK DESIGN VERIFIER 1

[. . . ] Simulink® Design VerifierTM 1 User's Guide How to Contact The MathWorks Web Newsgroup www. mathworks. com/contact_TS. html Technical Support www. mathworks. com comp. soft-sys. matlab suggest@mathworks. com bugs@mathworks. com doc@mathworks. com service@mathworks. com info@mathworks. com Product enhancement suggestions Bug reports Documentation error reports Order status, license renewals, passcodes Sales, pricing, and general information 508-647-7000 (Phone) 508-647-7001 (Fax) The MathWorks, Inc. 3 Apple Hill Drive Natick, MA 01760-2098 For contact information about worldwide offices, see the MathWorks Web site. Simulink® Design VerifierTM User's Guide © COPYRIGHT 2007­2010 by The MathWorks, Inc. The software described in this document is furnished under a license agreement. The software may be used or copied only under the terms of the license agreement. [. . . ] You can then use the Simulink Design Verifier software to prove whether such properties are valid for your model. The software performs a formal analysis of your model to prove or disprove the specified properties. If the software disproves a property, it provides a counterexample that demonstrates a property violation. Proof Blocks The Simulink Design Verifier software provides two blocks that allow you to specify property proofs in your Simulink models: · Proof Objective -- Define the values of a signal to prove · Proof Assumption -- Constrain the values of a signal during a proof Note Blocks from the Model Verification library in the Simulink software behave like a Proof Objective block during Simulink Design Verifier proofs. Therefore, you can use Assertion blocks and other Model Verification blocks to specify properties of your model. For more information about these blocks, see "Model Verification" in the Simulink Reference. Proof Functions The software provides two Embedded MATLAB functions to specify property proving for a Simulink Model or Stateflow chart: · sldv. prove -- Specifies a proof objective · sldv. assume -- Specifies a proof assumption These functions: · Identify mathematical relationships for proving properties in a form that can be more natural than using block parameters 10-2 About Property Proving · Support specifying multiple objectives, assumptions, or conditions without complicating the model · Provide access to the power of MATLAB · Support separation of verification and model design For an example using these proof functions, see the sldv. prove reference page. 10-3 10 Proving Properties of a Model Workflow for Proving Model Properties A recommended workflow for proving properties of your model is: 1 Ensure that your model is compatible for use with the Simulink Design Verifier software (for an example, see "Checking Compatibility of the Example Model" on page 10-7). 2 Instrument your model with blocks that specify proof objectives and proof assumptions (for examples, see "Instrumenting the Example Model" on page 10-11 and "Customizing the Example Proof" on page 10-22). Or, you can use Embedded MATLAB functions for proof objectives and assumptions; see "Proof Functions" on page 10-2. 3 Specify options that control how Simulink Design Verifier proves the properties of your model (for an example, see "Configuring Property-Proving Options" on page 10-14). 4 Execute the Simulink Design Verifier analysis and review the results (for examples, see "Analyzing the Example Model" on page 10-16 and "Reanalyzing the Example Model" on page 10-25). For an exercise that demonstrates this workflow, see "Proving Properties in a Model" on page 10-5 . 10-4 Proving Properties in a Model Proving Properties in a Model In this section. . . "About This Example" on page 10-5 "Constructing the Example Model" on page 10-6 "Checking Compatibility of the Example Model" on page 10-7 "Instrumenting the Example Model" on page 10-11 "Configuring Property-Proving Options" on page 10-14 "Analyzing the Example Model" on page 10-16 "Customizing the Example Proof" on page 10-22 "Reanalyzing the Example Model" on page 10-25 "Analyzing Contradictory Models" on page 10-26 About This Example The sections that follow describe a simple Simulink model, for which you prove a property that you specify using a Proof Objective block. This example demonstrates the property-proving capabilities of the Simulink Design Verifier software. The following workflow guides you through the process of completing this example. Task 1 2 Description Construct the example model. Ensure your model's compatibility with the Simulink Design Verifier software. Add a Proof Objective block to your model to prepare for its proof. "Constructing the Example Model" on page 10-6 "Checking Compatibility of the Example Model" on page 10-7 3 "Instrumenting the Example Model" on page 10-11 10-5 10 Proving Properties of a Model Task 4 Description Configure the Simulink Design Verifier software to prove properties. Prove a property of your model and interpret the results. Add a Proof Assumption block to customize the proof. Prove a property of your modified model and interpret the results. See. . . "Configuring Property-Proving Options" on page 10-14 "Analyzing the Example Model" on page 10-16 "Customizing the Example Proof" on page 10-22 "Reanalyzing the Example Model" on page 10-25 5 6 7 Constructing the Example Model In this task, you construct a Simulink model that you use throughout the remaining tasks. To complete this task, perform the following steps: 1 Create an empty Simulink model. 2 Copy the following blocks into your empty model window: · From the Sources library, an Inport block to initiate the input signal whose value the Simulink Design Verifier software controls · From the Logic and Bit Operations library, a Compare To Zero block to provide simple logic · From the Sinks library, an Outport block to receive the output signal 3 Connect these blocks such so your model appears similar to the following model: 10-6 Proving Properties in a Model 4 Save your model as example. mdl for use in the next task. Checking Compatibility of the Example Model In this task, you ensure that a model is compatible for use with the Simulink Design Verifier software. Specifically, you check the compatibility of the simple Simulink model that you created in the previous task. To complete this task, perform the following steps: 1 In your Simulink model window, select Tools > Design Verifier > Check Model Compatibility. [. . . ] For example, given a sufficiently large floating-point number x, the expression x==(x+1) is true; however, this expression never holds if x is a rational number. invalid test case A test case that does not satisfy its objectives. modified condition/decision coverage (MCDC) Measures the independence of logical block inputs and transition conditions associated with logical model objects during the simulation. When you set the coverage objective to MCDC, Simulink Design Verifier automatically enables every coverage objective for decision coverage and condition coverage as well. [. . . ]