Mathworks POLYSPACE MODEL LINK PRODUCTS 5 user guide

Download

PolySpace®Model L

User’s Guide

ink Products 5

How to Contact The MathWorks

www.mathworks. comp.soft-sys.matlab Newsgroup www.mathworks.com/contact_TS.html T echnical Support

suggest@mathworks.com Product enhancement suggestions

bugs@mathwo doc@mathworks.com Documentation error reports service@mathworks.com Order status, license renewals, passcodes

info@mathwo

com

rks.com

Web

Bug reports

Sales, prici

ng, 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.

PolySpace

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. No part of this manual may be photocopied or reproduced in any form without prior written consent from The MathW orks, Inc.

FEDERAL ACQUISITION: This provision applies to all acquisitions of the Program and Documentation by, for, or through the federal government of the United States. By accepting delivery of the Program or Documentation, the government hereby agrees that this software or documentation qualifies as commercial computer software or commercial computer software documentation as such terms are used or defined in FAR 12.212, DFARS Part 227.72, and DFARS 252.227-7014. Accordingly, the terms and conditions of this Agreement and only those rights specified in this Agreement, shall pertain to and govern theuse,modification,reproduction,release,performance,display,anddisclosureoftheProgramand Documentation by the federal government (or other entity acquiring for or through the federal government) and shall supersede any conflicting contractual terms or conditions. If this License fails to meet the government’s needs or is inconsistent in any respect with federal procurement law, the government agrees to return the Program and Docu mentation, unused, to The MathWorks, Inc.

Trademarks

MATLAB and Simulink are registered trademarks of The MathWorks, Inc. See

www.mathworks.com/trademarks for a list of additional trademarks. Other product or brand

names may be trademarks or registered trademarks of their respective holders.

Patents

The MathWorks products are protected by one or more U.S. patents. Please see

www.mathworks.com/patents for more information.

Revision History

March 2009 Online Only Revised for Version 5.3 (Release 2009a) September 2009 O nline Only Revised for Version 5.4 (Release 2009b) March 2010 Online Only Revised for Version 5.5 (Release 2010a)

Model Link Products User’s Guide

Getting Started with PolySpace Model Link

Products

Overview of PolySpace M odel Link Products ......... 1-2

Contents

Getting Started with Model Link Products

Overview Creating a Simulink Model and Generating Production

Code Starting the PolySpace Verification Fixing an Error in the Design and the Simulink Model Base Workspace vs. PolySpace Data Ranges

........................................ 1-3

.......................................... 1-3

................... 1-9

........... 1-3

........... 1-14

Advanced Setup Options

Advanced Setup ................................... 2-2

Handwritten Code Target Production Environment Creating a PolySpace Configuration File Template

................................. 2-2

..................... 2-3

...... 2-6

PolySpace Utilities

... 1-11

PolySpace Utilities Library ......................... 3-2

Overview of PolySpace Utilities Library Open Po ly Space Results PolySpace Enable COM Server PolySpace Menu PolySpace Project Configuration

.................................. 3-4

............................ 3-3

...................... 3-3

..................... 3-5

............... 3-2

iii

PolySpace Utilities Menu ........................... 3-8

PolySpace Commands Available in Batch Mode as

M-Functions

Archives Files Produced for the PolySpace

Verification

Template files located in MATLAB installation

directory\polyspace\ Files used in the model directory Auto-generated files in the model directory

.................................... 3-10

..................................... 3-12

............................ 3-12

..................... 3-13

............ 3-13

Code Generator Specific Information

PolySpace Model Link SL Product .................. 4-2

Overview Subsystems Default Options Data Range Specification Code Generation Options PolySpace Analysis Option s

........................................ 4-2

...................................... 4-2

................................... 4-2

........................... 4-3

......................... 4-4

iv Contents

PolySpace Model Link TL Product

Overview Subsystems Data Range Specification Lookup Tables Code Generation Options

........................................ 4-15

...................................... 4-15

........................... 4-15

.................................... 4-16

........................... 4-17

.................. 4-15

Glossary

Getting Started with PolySpace Model Link Products

• “Overview of P o lySpa ce Model Link Products” on page 1-2

• “Getting Started with Model Link Products” on page 1-3

1 Getting Started with PolySpace

Model Link Products

Overview of PolySpace Model Link Products

This manual describes how to use PolySpace®for Model-Based Design. The PolySpace Model Link™ SL and PolySpace Model Link TL products allow you to launch a PolySpace C verification from a Simulink Real-Time Workshop software.

PolySpace Model Link SL and PolySpace Model Link TL products provide automatic error detection for code generated from Simulink models. It consists of two principal components:

• A Simulink PolySpace library with associated blocks.

• A “Back to Mode l” extension in the Po ly Space Viewer th at allows direct

navigation from a runtime error in the auto-generated code to the corresponding Simulink block or Stateflow

Embedded Coder™ software, or dSPACE®TargetLink

model associated with

chart in the Simulink model.

1-2

Getting Started with Model Link Products

In this section...

“Overview” on page 1-3

“Creating a Simulink Model and Generating Production Code” on page 1-3

“Starting the PolySpace Verification” on page 1-9

“Fixing an Error in the Design and the Simulink Model” on page 1-11

“Base Workspace vs. PolySpace Data Ranges” on page 1-14

Overview

In this section, you will:

• Create a Simulink model and generate production code (For more

information, see the Real-Time Workshop Embedded Coder Getting Started Guide)

Getting Started with Model Link Products

• Start the PolySpace verification

Creating a Simulink Model and Generating Production Code

To create a Simulink model and generate production code:

1 Open MATLAB

2 Create a simple Simulink model, similar to the one below.

, then start Simulink software.

1-3

1 Getting Started with PolySpace

Model Link Products

1-4

Create the my_first_code model

3 Select File > Save,thennamethemodelmy_first_code.

4 Select View > Model Explorer.

The Model Explorer ope n s.

Getting Started with Model Link Products

5 Select Configuration Preferences, in the Model Hierarchy.

6 Select R

eal-Time W orkshop in the Configuration Preferences.

The Real-Time Workshop configuration parameters open.

7 Select the Real-Time Workshop General tab.

Set the Coder (

System target file to ert.tlc (Real Time Workshop Embedded

no auto configuration)).

1-5

1 Getting Started with PolySpace

Model Link Products

Change the code g ene rator to Real-Time Workshop®Embedded Coder™ software

8 Select the Report tab.

9 Select Create code-generation report, then select Code-to-model

Navigation.

1-6

Set Report Settings

Getting Started with Model Link Products

10 Select the Templates tab.

Temp lates Ta b

11 In the Custom templates section, clear Generate an example main

program.

12 Select the Interface tab.

1-7

1 Getting Started with PolySpace

Model Link Products

Interface Tab

1-8

13 In the Code interface section, select suppress error status in real-time

model data structure.

14 Click A pply in the lower-right corner of the window.

15 In the Configuration Preferences, select Solver.

The Solver configuration parameters appear.

Choose Fixed-step Solver

16 In the Solver options section, set the solver Type to Fixed-step.Then,set

the Solver to

Getting Started with Model Link Products

discrete (no continuous states).

17 Click Apply.

18 In the Simulink Model Window, select Tools > Real Time Workshop

>BuildModelto generate the production code.

19 Save your Simulink model.

Starting the PolySpace Verification

To Start the PolyS pace verification:

1 In the Simulink model window select Tools > PolySpace > PolySpace

for RTW Embedded Coder.

The PolySpace Analyser dialog box opens.

1-9

1 Getting Started with PolySpace

PolySpace Analyser Dialog Box

Model Link Products

1-10

Note The subsystem field is automatically populated with the name of the current subsystem, and the results directory is automatically set to

results_subsystem_name. If more than one subsystem is present in the

model, a subsystem selection dialog opens.

2 Click Start to start the verification.

The verification starts, and messages appear in the MATLAB Command window:

### PolySpace Technologies RTW Embedded Coder integration ### Version 1.4 ### Preparing verification ### Locating generated source files:

ert_main.c ok (c:\MatLAB704\toolbox\rtw\rtwdemos

\rtwdemo_examplemain_ert_rtw)

rtwdemo_examplemain.c ok (c:\MatLAB704\toolbox\rtw\rtwdemos \rtwdemo_examplemain_ert_rtw) ### Generating DRS table

### Get Parameters

Getting Started with Model Link Products

### Get Signals ### Starting verification

The exact messages depend on the code generator you use. However, the messages always have the same format:

• Name of code generator

• Version number of the plug-in

• List of source files

• DRS (Data Range Specification) information.

3 You can follow the progress of the verification in the MATLAB Command

window, and later using the PolySpace Spooler if you are performing a server verification.

Note Verification of this model takes about 7 minutes. A 3,000 block model will take approximately one hour to verify, or about 15 minutes for each 2,000 lines of generated code.

Fixing an Error i n the Design and the Simulink Model

After the verification completes, you can view the results using PolySpace Viewer.

Note If you perform a server verification, you must download your results from the server before you can view them. For more information, see “Downloading Results from Server to Client” in the PolySpace Products for C User’s Guide.

To view your results:

1 In the Simulink model window select Tools > PolySpace > PolySpace

Utilities > Open results.

Afterafewseconds,thePolySpaceVieweropens.

1-11

1 Getting Started with PolySpace

Model Link Products

Coding review progress view

Procedural

Variables

entities view

view

Selected check view

Source code

Call tree

view

1-12

2 Type CTRL-N to go to the next error.

Getting Started with Model Link Products

Overflow in the code

Orange Check in PolySpace®Viewer

3 Click on the orange check.

The check shows an overflow of the two entries. PolySpace software assumes that the values for entries are full range, and their multiplication can overflow.

1-13

1 Getting Started with PolySpace

4 Now, you must get back to the model to understand what needs to be fixed.

Click the first underlined blue HTML link near the check in the Source Code.

The Simulink model opens, highlighting the block with the error.

Model Link Products

1-14

Model with Highlighted Block

5 You now must fix the defect in the model. For example, you may come

to one of the following conclusions:

• It is a bug in the design— The developer should saturate the output,

providing this functionally makes sense bound the entries in the model, by adding blocks which will test the input values, and bound them accordingly.

• It is a bug in the specifications — The developer should bound the

entries, by giving them a range in Simulink software that PolySpace verification can take the ranges into account and turns the code green.

Base Workspace vs. PolySpace Data Ranges

After y ou examine the model, you can see a block whose signal range s are not in the expected range.

Getting Started with Model Link Products

• If its block is supposed to be robust against this range, it is a design bug.

Should the previous block be saturated? Should the signal be bounded with a “switch” block? It is up to the developer to decide the a ppropriate change in the model

• If the range is an input range of the model, the developer may wish to

give this informa t ion to the Simulink model, so that PolySpace tools ca n use that range as an entry.

Prerequisites

Have signals as ExportedGlobal.

Details of a signal

Update Range of Signals

To update your signal ranges:

1 Open model explorer, and go into the Base Workspace tab.

2 Create a signal “my_entry1”&“my_entry2.”

3 Bound it to -15 to 15. Specify its storage class to ExportedGlobal.

1-15

1 Getting Started with PolySpace

Signal in the “Base Workspace”

Model Link Products

1-16

4 Model with signals on entries:

Getting Started with Model Link Products

Model with signals my_entry1 and my_entry2 as “ExportedGlobal”.

Re-Generate Code and Launch the PolySpace Verification Again

To regenerate the code and relaunch the PolySpace verification:

1 Regenerate the code

Theentriesarenolongerpartofastructure, they are separated global each.

1-17

1 Getting Started with PolySpace

Model Link Products

1-18

Html re

port generator from Real-Time Workshop

2 Select Tools > PolySpace > PolySpace for RTW Embedded Coder.

The PolySpace Analyser dialog box opens.

Embedded Coder™ Software

Getting Started with Model Link Products

PolySpace Analyser Dialog Box

3 In results directory field enter results_my_first_code_bounded.

4 In the subsystem name field, enter my_first_code_bounded.

5 Click Start to start the verification.

6 Once verification is complete, select Tools > PolySpace > PolySpace

Utilities > Open results to view your results.

7 Examine the generated files in the PolySpace Viewer:

1-19

1 Getting Started with PolySpace

Model Link Products

Detail of generated files viewed in PolySpace®Viewer

Everything is green. PolySpace verification has confirmed that no Runtime Errors are present in the model.

Can You Find More Bugs in the Model?

To answ er this question, we nee d to now more about the tool, such as:

• Which windows of the PolySpace Viewer contain what information

• Which colors hide which messages

• How to find bugs using PolySpace Viewer

For more information, see “Reviewing Verification Results” in the PolySpace Products for C User’s Guide.

1-20

Advanced Setup Options

2 Advanced Setup Options

Advanced Setup

In this section...

“Handwritten Code” on page 2-2

“Target Production Environment” on page 2-3

“Creating a PolySpace Configuration File Te mplate” on page 2-6

Handwritten Code

FilessuchasS-functionwrappersare, by default, not part of the PolySpace verification. They should be added manually.

To add a file manually:

1 When starting the PolySpace verification, browse and add c-files to your

verification:

2-2

2 Select additional files by ticking “Enable additional file list,” then click

on “Select Files”.

A C File browser appears to add files to the PolySpace verification.

Advanced Setup

3 Select the appropriate c file and th en start the verifica t ion.

Target Production Environment

In Simulink software, you need to configure the target and cross-compiler specificities.

These parameters include:

• Size of the types fo r char, short, int (see Hardware implementation of the

model explorer)

2-3

2 Advanced Setup Options

Target selection in Simulink®Configuration Parameters

• Cross compiler flag (-D), and library include (-I), implicitly defined when -

for instance - the cross compiler is setup via the “mex -setup” command.

2-4

Advanced Setup

Cross compiler settings in MATLAB®Command Window

PolySpace settings work exactly the same way, you will need to perform the following tasks (they will be detailed step by step in the next sections).

1 define the same parameters for your cross compiler and target.

2 save th is in a t emplate Poly S p ace configuration file and set t h is template to

be the default configuration file for every P oly Space verification.

Why does this matter?

• For the PolySpace verification, an overflow on an integer type does not

mean the same when the size of an integer is 16 b its or 32 bits.

2-5

2 Advanced Setup Options

• PolySpace software needs the cross compiler header files, as th ey contain

definitions of types, macros, used by the application, whether the application made of generated code or hand written code.

For more information, refer to and “Option Descriptions” in the PolySpace Products for C Reference.

Creating a PolySpace Configuration File Template

To Create a configuration file template:

1 In the Simulink model window, select Tools > PolySpace > PolySpace

Utilities > Configure project.

The PolySpace Launcher interface o pens, allowing you to customize the target and cross compiler.

Target and cross com piler settings in PolySpace®tools

2 The

-target option defined the size of types. You can configure a custom

get by selecting

tar

mcpu (advanced) at the bottom of the drop-down list

2-6

Advanced Setup

3 You can configure cros s compiler settings by clicking on the -D options.

Note MATLAB_MEX_FILE is a directive option that is needed when the LCC

cross-compiler is specified. Defining templates can be use in all subsequent verification.

4 Save the co nfiguration file and close the interface.

le in

5 Copy the fi

6 Rename it in my_cross_compiler.cfg (It could be any other name).

<matlabroot>/polyspace/cfg directory.

7 Type in the MATLAB command window:

PolySpa ('C:\MA

Create a template configuration file

ceSetTemplateCFGFile TLAB\R2006b\polyspace\cfg\my_cross_compiler.cfg')

This configuration file can now be used as a template for all subsequent verification.

2-7

2 Advanced Setup Options

2-8

PolySpace Utilities

• “PolySpace Utilities Library” on page 3-2

• “PolySpace Commands Available in Batch Mode as M-Functions” on page

3-10

• “Archives Files Produced for the PolySpace Verification” on page 3-12

3 PolySpace

Utilities

PolySpace Utilities Library

In this section...

“Overview of PolySpace Utilities Library” on page 3-2

“Open PolySpace Results” on page 3-3

“PolySpace Enable COM Server” on page 3-3

“PolySpace Menu” on page 3-4

“PolySpace Project Configuration” on page 3-5

“PolySpace Utilities Menu” on page 3-8

Overview of PolySpace Utilities Library

The PolySpace Utilities Library consists of four blocks:

• Open PolySpace Results

3-2

• PolySpaceEnableCOMServer

• PolySpace Menu

• PolySpace Project Configuratio n

They can either be run directly from the Simulink library browser or dragged into a Simulink model (see next figure).

PolySpace®Utilities Library

PolySpace®Utilities

Open PolySpace Results

This option allows the results of the PolySpace verification to be viewed and easy nav igation with a right click from the PolySpace results to an element in the Simulink model.

PolySpace Enable COM Server

This block is called by default with the “Open PolySpace Results” block. This block is mandatory when The PolySpace Viewer is opened outside a Simulink session to enable the Back to Model feature inside the Viewer.

3-3

3 PolySpace

Utilities

Note If you do not have administrator rights to your system, you may receive an error when using the Back to Model feature in the Viewer. This occurs because the PolySpace Viewer cannot call the not have administrator rights to your system, ask your system administrator to run the command use with PolySpace software.

matlab /regserver on the version of MATLAB you

regserver command. If you do

PolySpace Menu

The menu consists of two sections, the first for managing the verification and the second for configuring the tools and documentation.

3-4

PolySpace®Menu

Analysis Management

Analysis management contains the following options:

• Configure project – Opens the PolySpace configuration dialog, for more

information see next section.

• Launch spooler – Opens the PolySpace spooler. For more information,

see “Running Verifications o n PolySpace Server”in the PolySpace Products for C User’s Guide .

PolySpace®Utilities Library

• Open results – Opens the PolySpace Viewer with the last available

results. If the verification has been done on the server, download in g them first is required before clicking on this button. It is recommended to not change the proposed directory during download.

• Stop local verification – Stops a verification running on the local

machine. If the verification has been remotely spooled this option will only work during the compilation phase before the verification is sent to the server. However, you can click the Launch spooler button and stop the verification from the spooler dialog.

General Options

Tools & Documen t ati o n contains the following option s:

• Don’t use automatic stubs – Enables/disables PolySpace automatic

stubbing of certain blocks behavior. This behavior depends on the code generator being used and is describedinthedocumentationspecificto your code generator below.

• Don’t check solver – Disables the check of the solver used with Re al-Time

Workshop Embedded Coder software.

3-5

3 PolySpace

Utilities

PolySpace Project Configuration

Clicking on “Project configuration” starts a cut-down PolySpace launcher (see next figure).

Next figure allows the configuration of the PolySpace project. For example setting items such as the processor type the code has been generated for, Compilation flags etc. The first time the tool is run a template configuration is created with the following options set:

-continue-with-existing-host

-ignore-float-rounding

-OS-target no-predefined-OS

-allow-ptr-arith-on-struct

-results-dir results

Other options are automatically set depending on the code generator being used. See the docume ntation for specific code generators below for more information.

3-6

PolySpace®Utilities Library

Project Configuration Interface

3-7

3 PolySpace

Utilities

PolySpace Utili

The PolySpace ut Library directl

To access the ut Utilities fro

The Utilities menu contains the following options:

• Open results – Opens the PolySpace Viewer with the last available results.

Configure project – Opens the PolySpace configuration dialog, for more

information see next section.

y from the Simulink model window.

m the model window.

ties Menu

ilities menu allows you to access the options in the PolySpace

ilities menu, select Tools > PolySpace > PolySpace

3-8

• Stop local verification – Stops a verification running on the local

machine. If the verification is run on the server, this option only works during the compilation phase before the verification is sent to the server. However, you can click the Launch spooler button and stop the verification from the spooler dialog.

• Launch spooler – Opens the PolySpace spooler. For more information,

see “Running Verifications o n PolySpace Server”in the PolySpace Products for C User’s Guide .

• Don’t use automatic stubs – Specifies that the verification will not

generate stubs. By default, PolySpace verification stubs all functions. Using this option allows you to use manual stubbing. For more information, see “Stubbing”in the PolySpace Products for C User’s Guide.

PolySpace®Utilities Library

• Don’t check solver – Specifies that the model be verified regardless of the

type of solver selected. To ensure o ptimal precision and performance, the software checks that the model uses a fixed-step discrete solver. Selecting this option disables this check.

• Enable initialization function – S pecifies that the

is called before the

_step function. This can reduce orange checks because

_initialize function

the f unctions are called in a more realistic order. When this option is not enabled (default), functions are called in random order.

• Help – Opens the PolySpace documentation.

3-9

3 PolySpace

Utilities

PolySpace Commands Available in Batch Mode as M-Functions

You can also run

Command

PolySpaceForEmbeddedCoder

PolySpac

PolySpaceSpooler

PolySpaceViewer

eForTargetLink

the following commands from the command line.

Description

Launch PolySpace verification on code generated by Real-Time Workshop Embedded Coder software

Launch Pol generate

Inspect the queue of the remotely sent verification over the server

Launch PolySpace Viewer

ySpace on code

dbyTargetLink

Icon

PolySpaceSetTemplateCFGFile

PolySpaceGetTemplateCFGFile

3-10

Selectatemplatefilein batch mode

Get the currently selected template file (empty by default)

PolySpace®Commands Available in Batch Mode as M-Functions

Command

PolySpaceReconfigure

ver

Example with EmbeddedCoder:

Suppose that you open a Simulink model with the name

Enter window.

The verification starts.

Description

Icon

In case of a PolySpace release update without enabling the MATLAB plug-in

Displays the PolySpace For Model-Link Version number along with other MathWorks product information

example.mdl.

PolySpaceForEmbeddedCoder('example') in the MATLAB Command

3-11

3 PolySpace

Utilities

Archives Files Produced for the PolySpace Verification

In this section...

“Template files located in MATLAB installation directory\polyspace\” on page 3-12

“Files used in the model directory” on page 3-13

“Auto-generated files in the model directory” on page 3-13

Template files located in MATLAB installation directory\polyspace\

When a verification is first performed the tool copies the following two files into the local model directory. On subsequent verifications the files are not copied again meaning it is OK to mo del the copies in the model directory.

•

cfg\templateEmbeddedCoder.cfg —Thisfileiscopiedtothe

model_directory/model_name-polyspace.cfg at the start of the first verification of the model. It contains the template PolySpace configuration settings to support the TargetLink code generator. The templateTargetLink.cfg file can be updated with site specific settings, to ease verification of new models.

3-12

A MATLAB command exists to change the name/location of the file which contains the template configuration:

PolySpaceSetTemplateCFGFile(config_filename)

This is most useful when the PolySpace verification is started as part of an automated process. Here the process would set the template configuration file to use, erase the local copy in the model directory and then start the PolySpace verification.

•

stub\ppcom_ec.sh — This file is copied to the model_directory/ppco m_ec.sh

at the start of the first verification of a model. The file is not recopied for subsequent verifications. It is used to stub lookup table types ( only interpolation, not extrapolation) to improve the accuracy of verification results.

Archives Files Produced for the PolySpace®Verif i c a ti on

Files used in the

• model-name-pol

this file is cop directory\pol a verificatio Project Confi PolySpace Ana the current m

•

ppcom_ec.sh

command.

polyspace_

•

Advanced op box. This o together w lookup tab additiona list of ex

Auto-ge

These fi started

l file list option needs to be set together with configuring the

tra files to analyze.

nerated files in the model director y

les are generated from the model for each verification when it is

, and do not need archiving:

yspace.cfg

ied from the MATLAB installation

yspace\cfg\templateEmbeddedCoder.cfg file the first time

n is run on a m odel. It is subsequently mo dified by the

guration block, or the Configure button in the option in the

lyzer dialog. It contains the PolySpace settings for verifying

odel.

— The PolySpace Embedded Coder post preprocessing

additional_file_list.txt

tion, Select Files is used in the PolySpace Analyzer dialog

ption allows files that are not part of the model to be analyzed ith the model. Fo r example these files could con tain custom le code, custom stubs, device driver code etc. The Enable

model directory

— As mentioned above

— This file i s created if the

•

model n

from th

•

polysp

direc

•

polys

•

mode

the P

ame_drs.txt

e model.

ace_include_dir_list.txt

tories extracted from the mode.

pace_file_list.txt

l name_last_parameter.txt

olySpace Analyzer dialog box.

— The DRS information extracted automatically

— List of file contained in the model to analyze

— List of compilation include

— The last set of parameters used in

3-13

3 PolySpace

Utilities

3-14

Code Generator Specific Information

• “PolySpace Model Link SL Product” on page 4-2

• “PolySpace Model Link TL Product” on page 4-15

4 Code Generator Specific Information

PolySpace Model Link SL Product

In this section...

“Overview” on page 4-2

“Subsystems” on page 4-2

“Default Options” on page 4-2

“Data Range Specification” on page 4-3

“Code Generation Options” on page 4-3

“PolySpace Analysis Options” on page 4-4

Overview

The PolySpace Model Link SL product has been tested with Real-Time Workshop Embedded Coder software — see the Installation Guide for more information.

4-2

Subsystems

A dialog will be presented after clicking on the PolySpace for Embedded Coder block if multiple subsystems are present in a diagram. Simply select the subsystem to analyze from the list. The subsystem list is generated from the directory structure from the code that has been generated.

Default Options

The following default options are set by the tool:

ath to source code

-I

-desktop

-D PST_ERRNO

atlabroot\polyspace\include

-I m

-I matlabroot\extern\include

-I matlabroot\rtw\c\libsrc matlabroot\simulink\include

-I

-I matlabroot\sys\lcc\include

PolySpace®Model Link™ SL Product

Note matlabroot is the MATLAB tool installation directory.

Data Range Specification

The software automatically creates a PolySpace Data RangeSpecification (DRS) file using information from the MATLAB workspace. This DRS information is used to initialize each global variable to the range of valid values, as defined by the min-max information in the workspace.

The main sources o f information are Simulink. sig nals and Simulink.parameters.

You can also manually define a DRS file using the PolySpace Launcher. If youdefineaDRSfile,thesoftwareappendstheautomaticallygenerated information to the DRS file you create. Manually defined DRS information overrides automatically generatedinformationforallvariables.

Code Generation Options

This section describes recommended configuration parameter settings for Real-Time Workshop options for optimum use of PolySpace verification.

In the Real Time Workshop tab:

1 Select Generate HTML report.

2 Select Include hyperlinks to model.

Note If you do not set this option, navigation from PolySpace results to

the model will not work.

3 Set the system target file to be an appropriate ert.tlc (use the b row s e

button to locate).

software. The MathWorks recommends using these

4-3

4 Code Generator Specific Information

This is an indication that the code generator is Real-Time Workshop Embedded Coder software (and not just Real-Time Workshop software, used for rapid prototyping).

In the Solver tab:

1 Set the solver Type to Fixed-step,

2 Set the Solver to discrete (no continuous state).

This specifies that the code is generated for a target, and not for a simulation based on continuous timing.

In the Interface panel tab:

1 Ensure that Generate reusable code is not selected.

Setting this option will generate more warnings in the PolySpace results.

PolySpace Analysis Options

This section describes reco mmended Analysis options for verifying code generated with Real-Time Workshop Embedded Coder software. The MathWorks recommends setting these options in your PolySpace project before verifying generated code.

If y ou have PolySpace Model Link SL software, you can specify the Analysis options for your PolySpace Project by selecting Tools > PolySpace > PolySpace Utilities > Configure P roject in the Simulink model window.

Option

General Options

-author <your name>

4-4

Recommended Value

Comments

Specifies the name of the author of the verification

PolySpace®Model Link™ SL Product

Option

-date <date stamp>

-desktop

Recommended Value

Selected – When checking MISRA Compliance (code analysis).

Not Selected –When checking runtime errors (code verification)

-I

-prog <session identifier>

See Comments Specifies the name of a folder

Comments

Specifies a date stamp for the verification in

dd/mm/yyyy

format. This information is labelled in the GUI as Date. You can specify alternate date formats using Edit > Preferences.

Specifies whether verification occurs on the PolySpace Client or PolySpace Server. The MathWorks recommends using the Client to perform MISRA analysis and the Server for code verification.

to include when compiling C sources. You can specify only one folder for each

I,butcan

use the option multiple times.

A script to automatically determine

buildInfo is available

-I based on

Specifies the application name. Use characters valid for Unix file names.

This information is labelled in the GUI as Session identifier.

For example,

New_Project.

4-5

4 Code Generator Specific Information

Option

-results-dir <results dir>

-sources

-sources-list-file

Recommended Value

See Comments Specifies a list of source files

Comments

Specifies the directory in which PolySpace software saves verification results. You can specify a relative path. However, be careful if you plan to launch verification remotely over a network, or if you plan to copy the project configuration file using the "Save as" option.

to be verified. You must enclose the list of source files in double-quotes, separated by commas.

•

-sources "file1[ file2[ ...]]"

(Linux and

Solaris™) -

•

-sources "file1[,file2[, ...]]"

(Windows®, Linux and Solaris)

4-6

•

-sources-list-file file_name

(not a graphical

option)

You can specify multiple files using UNIX® standard wildcards.

The software compiles the source files in the order in which you specify them.

If you do not specify any files, the software verifies all files

PolySpace®Model Link™ SL Product

Option

-verif-version

Recommended Value

1.0

Target/Compilation Options

-d

-OS-target Visual

See Comments Defines macro compiler flags

Comments

in the source directory in alphabetical order.

Note The specified files must have valid extensions:

*.(c|C|cc|cpp|CPP|cxx|CXX)

A script to automatically determine

buildInfo is available.

-sources based on

Specifies the version identifier of the verification. You can use this option to identify multiple verifications of the same project. This information is identified in the GUI as the Version.

used during compilation. Specifies the operating system

Use one target for PolySpace stubs.

RTW generated file.

This information allows the verification to use appropriate

PolySpace Model Link SL does system definitions during

not do this by default. preprocessing in order to

d for each line of the

defines.txt

analyze the included files properly.

4-7

4 Code Generator Specific Information

Option

-target i386

Compliance with standards Options

-dos

Recommended Value

Selected

Comments

Specifies the target processor type. Thisallowsthe verification to consider the size of fundamental data types and the endianess of the target machine.

You can configure and specify generic targets. For more information, see Setting Up Project for Generic Target Processors in the PolySpace Products for C User’s Guide.

You must select this option if the contents of the include or source directory comes from a DOS or Windows file system. The option allows the verification to deal with upper/lower case sensitivity and control characters issues. Concerned files are:

4-8

• Header files – All include

folders specified (

• Source files – All source

files selected for the verification ( option)

-I option)

-sources

PolySpace®Model Link™ SL Product

Option

-misra2

-includes-to-ignore <MSVC dir>\VC\include

Recommended Value

[all-rules | file_name]

Comments

Specifies that the software checks coding rules in conformity to MISRA-C:2004. All MISRA checks are included in the log file of the verification. Options:

•

all-rules –Checksall

available MISRA C® rules. Any violation of MISRA C rules is considered a warning.

•

filename –Specifiesan

ASCII file containing a list of MISRA® rules to check.

Specifies files or folders that are excluded from MISRA rules checking (all files and subfolders within the selected folder). This option is useful when you have non-MISRA C conforming include headers.

PolySpace inner settings Options

-main-generator-writes-variablespublic

Specifies how the generated main initializes global variables.

By selecting public, every variable except

const variables are assigned a

static and

"random" value, representing the full range of possible values

4-9

4 Code Generator Specific Information

Option

-main-generator-calls unused

-ignore-float-rounding

Recommended Value

Selected Specifies how the verification

Comments

Specifies how the generated main calls functions.

By selecting unused, e very function is called by the generated main unless it is called elsewhere by the code undergoing verification.

rounds floats.

If this option is not selected, the verification rounds fl oats according to the IEEE® 754 standard – simple precision on 32-bits targets and double precision on targets that define double as 64-bits.

When you select this option, the verif ica tion perform s exact computation.

Selecting this option can lead to results that differ from "real life," depending on the actual compiler and target. Some paths may be reachable (or not reachable) for the verification while they are not reachable (or are reachable) for the actual compiler and target.

Precision/Scaling Options

4-10

However, this option reduces the number of unproven checks caused by float approximation.

PolySpace®Model Link™ SL Product

Option

-O 2

Recommended Value

Comments

Specifies the precision level for the verification.

Higher precision levels provide higher selectivity at the expense of longer verificat ion time.

The MathWorks recommends you begin with the lowest precision level. You can then address red errors and gray code before relaunching PolySpace verification using higher precision levels.

Benefits:

A higher precision level contributes to a higher selectivity rate, making results review more efficient and hence making bugs in the code easier to isolate.

The precision level specifies the algorithms used to model the program state space during verification:

•

-O0 corresponds to static

interval verification.

•

-O1 corresponds to complex

polyhedron model of domain values.

•

-O2 corresponds to more

complex algorithms to closely model domain values (a mixed approach with

4-11

4 Code Generator Specific Information

Option

-from scratch

Recommended Value

Comments

integer lattices and complex polyhedrons).

•

-O3 is suitable only for

units smaller than 1,000 lines of code. For such code, selectivity may reach as high as 98%, but verification maytakeuptoanhourper 1,000 lines of code.

Specifies the phase from which verification starts.

You can use this option on an existing verification to elaborate on the results that you have already obtained. For example, if a verification ran

-to pass1, you can restart

the verification

-from pass1

to reduce verification tim e.

Note the following:

4-12

-to

c-compile

– When checking

MISRA compliance only.

pass0

• This option can be used only

for client verifications. All server verifications start from

scratch.

• All options other than

scratch can be used only

if the previous verification was launched using the option

-keep-all-files.

• You cannot use this option if

you modify the source code between verifications.

Specifies the phase after which the verification stops. Each

PolySpace®Model Link™ SL Product

Option

Recommended Value

– When verifying code for the first time.

pass4 –Whenperforming

subsequent verifications of code.

Comments

verification phase improves the selectivity of your results, but increases the overall verification time.

Improved selectiv ity can make results review more efficient, and hence make bugs in the code easier to isolate.

The MathWorks recommends you begin by running

pass0 Analysis level 0

(Software Safety

-to

)Youcan then address red errors and gray code before relaunching verification using higher integration levels.

Default P olySpace Analysis Options

When using the PolySpace Model Link SL product, the software sets the following Analysis options by default:

-sources path_to_source_code

-desktop

-D PST_ERRNO

-I matlabroot\polyspace\include

-I matlabroot\extern\include

-I matlabroot\rtw\c\libsrc

-I matlabroot\simulink\include

-I matlabroot\sys\lcc\include

-ignore-float-rounding

-OS-target no-predefined-OS

-allow-ptr-arith-on-struct

-results-dir results

4-13

4 Code Generator Specific Information

Note matlabroot is the MA TLAB installation directory.

4-14

PolySpace Model Link TL Product

In this section...

“Overview” on page 4-15

“Subsystems” on page 4-15

“Data Range Specification” on page 4-15

“Lookup Tables” o n page 4-16

“Code Generation Options” on page 4-17

Overview

The PolySpace Model Link TL product has been tested with the some release of the dSPACE Data Dictionary version and TargetLink Code Generator - see the Installation Guide for more information.

As the PolySpace Model Link TL product extracts information from the dSPACE D ata Dictionary remember to regeneratethecodebeforeperforming a PolySpace verification. This ensures that the Data Dictionary has been correctly updated.

PolySpace®Model Link™ TL Product

Subsystems

A dialog will be presented after clicking on the PolySpace for TargetLink block if multiple subsystems are present in a diagram. Simply select the subsystem to analyze from the list.

Data Range Specification

The tool a uto m atically creates PolySpace Data RangeSpecification (DRS) information using the dSPACE Data Dictionary for each global variable. This DRS information is used to initialize each global variable to the range of valid values as defined by the min-max information in the data dictionary. This allows PolySpace software to model every value that is legal for the system during its verification. Further the Boolean types are modeled having a minimum value of 0 and a maximum of 1. Defining the min-max information carefully in the model can help PolySpace verification to be more precise significantly because only range of reels values are analyzed.

4-15

4 Code Generator Specific Information

DRS cannot be applied to static variables. Therefore, the compilation flag s

static=

is set automatically. It has the effect of removing the static keyword

-D

from the code. If you hav e a problem with name clashes in the global name space you may need to either rename one of or variables or disable this option in PolySpace configuration.

Lookup Tables

The tool by default provides stubs for the lookup table functions. This behavior can be disabled from the PolySpace menu — see “PolySpace Menu” on page 3-4 for more information. The dSPACE data dictionary is used to define the range of their return values. Note that a lookup table that uses extrapolation will return full range for the type of variable that it returns.

Default Options

The following default options are set by the tool:

-I path to source code

-desktop

-D PST_ERRNO

-I dspaceroot\matlab\TL\SimFiles\Generic

-I dspaceroot\matlab\TL\srcfiles\Generic

-I dspaceroot/matlab\TL\srcfiles\i86\LCC

-I matlabroot\polyspace\include

-I matlabroot\extern\include

-I matlabroot\rtw\c\libsrc

-I matlabroot\simulink\include

-I matlabroot\sys\lcc\include

4-16

Note dspaceroot and matlabroot are the dSPACE and MATLAB tool installation directories respectively.

PolySpace®Model Link™ TL Product

Code Generation

From the TargetL code” and desele attributes”.

When installi variable has b ’C:\dSPACE\M

ink Main D ia log, it is recomm ended to set the option “Cl ean

ct the option “Enable sections/pragmas/inline/ISR/user

ng the PolySpace Model Link TL product, the tlcgOptions

een updated with ’PolyspaceSuppo rt’, ’on’ (see variable in

atlab\Tl\config\codegen\tl_pre_codegen_hook.m’ file).

Options

4-17

4 Code Generator Specific Information

4-18

Glossary

Atomic

In computer programming, atomic describes a unitary action or object that is essentially indivisible, unchangeable, whole, and irreducible.

Atomicity

In a transaction involving two or more discrete pieces of information, either all of the pieces are committed or none are.

Batch mode

Execution of PolySpace from the command line, rather than via the launcher Graphical User Interface.

Mathworks POLYSPACE MODEL LINK PRODUCTS 5 user guide

Specifications and Main Features

Frequently Asked Questions

User Manual