Verification And Validation Solutions For High Integrity Systems

Verification and Validation Solutionsfor High Integrity SystemsTiffany LiangApplication EngineerMathWorks 2015 The MathWorks, Inc.1

Recommended WorkflowDetecting errors early in the development cycleModel Design・Simulation(SL/SF)Model Comparison・Merge(Report Generator)Report Generation(Report Generator)Interface to RequirementsManagement Tool (SLVV)Formal Verification (SLDV)RequirementsExecutableRequirements ModelModel Guideline Check (SLVV)Model Coverage (SLVV)Test Case Generation (SLDV)Design Error Detection (SLDV)Implementation Model(Fixed-point)Source CodeAuto Code-Generation (EC)Traceability Report (EC)SIL/PIL Test（EC）Code Coverage（EC）Static Code Analysis(Polyspace)Object CodeConfiguration Management (Simulink Project)2

MathWorks benefitsEarly verification and Validation・Able to form small V-loops・Able to detect errors earlyin the development cycleRequirementsExecutableRequirements Linking (SLVV)Formal Verification (SLDV)Model Guideline Check (SLVV)Model Coverage Test (SLVV)Test Case Auto-Generation(SLDV)Report Auto-Generation(Report Generator) Model Code consistencyRequirements Modelallows for Simulink simulationresults to be considered “truth”. Early model verification isImplementation Modelpossible due to the ability to(Fixed-point)investigate floating-pointmodels Large team development madeSource Codeeasy through highlycustomizable tool chain Errors in object code detectedeasily through synchronizationObject Codebetween simulations andSILS/PILSSILS/PILS (EC)Runtime ErrorIdentification(Polyspace)3

Examples of High Reliability ApplicationsAirbags Unintended braking during operation Operational delay following impact250 CANmessageswith 2500individualAntiskid BrakessignalsVehicle-to-vehicle distance control Insufficient deceleration within required time Unintended asymmetrical brakingSource: K. Grimm: Software-Technologie in der Automoboilindustrie. 19. HTAGUNGin der Praxis,Sources:ISO 26262-1:2011Wien, Austria, May 2004Electronic Parking Brake4

Example: Door Lock Control SystemDoor Lock Control Auto-lock when vehicle in motion Auto-unlock during emergencies250 CANmessageswith 2500individualsignals5

Our First TopicInterface to RequirementsManagement Tool (SLVV)Formal Verification (SLDV)RequirementsModel Design・Simulation(SL/SF)Model Comparison・Merge(Report Generator)Report Generation(Report Generator)ExecutableRequirements ModelModel Guideline Check (SLVV)Model Coverage (SLVV)Test Case Generation (SLDV)Design Error Detection (SLDV)Implementation Model(Fixed-point)Source CodeAuto Code-Generation (EC)Traceability Report (EC)SIL/PIL Test（EC）Code Coverage（EC）Static Code Analysis(Polyspace)Object CodeConfiguration Management (Simulink Project)6

Door Lock Control Software Requirements7

Door Lock ModelSimulink / StateflowIncreased Readability /Productivity throughGraphical ModelingDoor LockRequest FunctionDiagnosticFunctionDiagnostic FunctionState Transition Diagram8

Door Lock Test ModelSimulink / SimscapeAble to execute various testsusing the control modelModel Block used to call control modelTest InputFail On/OffSwitchPlant ModelSimulation vs.ExpectedResultsComparison9

Requirements & Logic Testing through SimulationSimulink / Stateflow Early verification of entire system incl. plant behavior Investigation of failure/anomaly modes (difficult on H/W)Test data definition in Signal BuilderSimulation Results10

MATLAB/Simulink ProductsMATLAB Easy data processing Concise programminglanguage Abundant mathematicalfunctions ・ file I/O 2-D/3-D visualizationfunctionalityTechnical ComputingEnvironmentSimulinkStateflow Block diagram modeling Abundant block library High-precision time simulation Flowcharts, State Diagrams,State Transition TablesModel-Based DesignEnvironment11

Model Difference ComparisonsSimulink Report Generator Generate reports on difference comparisons between 2 models– Compatible with Simulink Project and version management software（i.e. Subversion）Green：Component mismatchRed：Parameter mismatch12

The Next TopicInterface to RequirementsManagement Tool (SLVV)Formal Verification (SLDV)RequirementsModel Design・Simulation(SL/SF)Model Comparison・Merge(Report Generator)Report Generation(Report Generator)ExecutableRequirements ModelModel Guideline Check (SLVV)Model Coverage (SLVV)Test Case Generation (SLDV)Design Error Detection (SLDV)Implementation Model(Fixed-point)Source CodeAuto Code-Generation (EC)Traceability Report (EC)SIL/PIL Test（EC）Code Coverage（EC）Static Code Analysis(Polyspace)Object CodeConfiguration Management (Simulink Project)13

Ensure TraceabilityClarification of effectsRequirement Model Test of requirement changesSimulink Verification & ValidationWhat is beingchecked?What is being tested?What is beingmodeled?14

Model Coverage for MeasuringCheck forinsufficient testingTest Completeness LevelSimulink Verification & ValidationCumulativecoverage resultson multiple testsIdentify areas ofmissing coverage15

Generate Tests for Full Model CoverageSimulink Design Verifier Automatic test generation Suitable for equality tests※ Able to generatemissing tests basedon user-defined testsTest Harness ModelAuto-generatedTest Data16

Identification of Software Design ErrorsSimulink Design Verifier Check for risks of software design errorsprior to implementationInteger overflow, division by zero, range violations, dead logicOverflow IdentifiedNo risk of overflowFixExample: Modify blockparameter17

Model Verification & Validation ProductsSimulink Verification and ValidationTM (SLVnV)Measure Model CoverageTraceabilityModel Checker (Model Advisor)Model to RequirementTT,TF,FTModel CoverageReport Decision Condition MC/DCTest Data Sufficiency CheckWordExcelDOORSMKS IntegrityRequirement to Model GUI for Model Checks Automate correctionson warnings Report Generation Add Custom Checks(Word/Excel/DOORS/MKS Integrity )Requirement Sufficiency CheckAutomate Model CheckingSimulink Design VerifierTM (SLDV)Design Error DetectionAuto-Generate Test CasesController ModelAuto-detect designerrors Division by zeroRange overflowDeadl LogicSaturation overflowOut of bounds accessAutomate Error DetectionProperty Proving (Formal ification Model100% Coverage Test DataCertify Correct Behavior18

The Final TopicInterface to RequirementsManagement Tool (SLVV)Formal Verification (SLDV)RequirementsModel Design・Simulation(SL/SF)Model Comparison・Merge(Report Generator)Report Generation(Report Generator)ExecutableRequirements ModelModel Guideline Check (SLVV)Model Coverage (SLVV)Test Case Generation (SLDV)Design Error Detection (SLDV)Implementation Model(Fixed-point)Source CodeAuto Code-Generation (EC)Traceability Report (EC)SIL/PIL Test（EC）Code Coverage（EC）Static Code Analysis(Polyspace)Object CodeConfiguration Management (Simulink Project)19

Generate Code from Controller ModelEmbedded Coder Auto-generate C-code of high readability/efficiency Option settings for variable attributes, functionsettings, code style, etc. Auto-generate scaling for fixed-point designif (LockMode FAILURE) {LockRequest FALSE;Auto-generate } else {codeLockRequest ((spd time Speed time) &&Engine ON && (!Airbag ON));}20

Ensuring Traceability betweenRequirements, Models, and CodeEmbedded Coder / Simulink Report Generator Reflect modelspecifications ingenerated code Distribute reports withmodel views (html)Code Document LinkCode Model LinkCode Generation Report21

Model Code Equality Checks（SIL/PIL, Back 2 Back Test）Embedded CoderEfficient testing by reuse of modelverification test dataModel/Code ResultsComparisonExisting data/SLDVgenerated test dataModel/CodeSelection※ Test automation through Simulink Test.22

Tool Chain Example: Product ListProductFunctionalityUsageSimulinkModeling: Controller BlockModelingModule/Integration TestStateflowModeling: State Transitions,Flow ChartsModelingFixed-Point DesignerModeling: Fixed-Point ProcessingModelingSimulink Verificationand ValidationModel CoverageRequirements InterfaceModel AdvisorModule/Integration TestReview and Static AnalysisSimulink Design VerifierProperty ProvingTest GenerationDesign Error DetectionReview and Static AnalysisEmbedded CoderCode GenerationPIL Test/CGVBullseye/LDRA IntegrationTraceability ReportCode GenerationEquality TestingCode Coverage MeasurementIEC Certification KitTraceability Matrix GenerationTemplates for CertificationISO26262 SupportSimulink ReportGeneratorReport Editing and GenerationReport GenerationModel Comparison/Merge23

Proving Source Code CorrectnessPolyspace Code Prover: Static Code VerificationGreen: reliable Quality– Prove absence of runtimeerrors (RTEs)safe pointer accessstatic void pointer arithmetic (void) {int array[100];int *p array;int i;for (i 0; i 100; i ) {*p 0;p ;variable ‘I’ (int32): [0 . 99]}assignment of ‘I’ (int32): [1 . 100]Red: faultyout of bounds error– Measure, Improve, Manage Usage– No need to compile, execute,or generate test cases– Supports：C/C /Ada ProcessGray: deadunreachable codeOrange: unprovenmay be unsafe for someconditions– Early detection of RTEsi get bus status();– Analyze both hand-code and Purple: violationauto-generated codeMISRA-C/C or JSF – Measure code reliabilityif (get bus status() 0) {if (get oil pressure() 0) {*p 5;} else {i ;}}code rulesif (i 0) {*(p - i) 10;}}Range datatool tipAnalyze all executable paths to detect errors and prove the absence of errors24

ISO26262 Functional Safety Standard Functional safety standard for automotive equipment Based on IEC61508 Description of purpose and requirements for development– Activities for development process （Software safety life cycle）– Development and verification tools （Tool qualification） Description of new software engineering concepts– Model-based development– Early verification and validity checks– Automatic code generation25

Model-Based Design Benefits（ISO26262 excerpt）The seamless utilization of models facilitates a highly consistent and efficient development.26

MathWorks Solution: SummaryUsing Models to Detect Errors Early andIncrease Efficiency・Able to form small V-loops・Able to detect errors earlyin the development cycleRequirementsRequirements Linking (SLVV)Formal Verification (SLDV)Executable Mode Code consistency allows Requirements Modelfor Simulink simulation results tobe considered “truth”. Early model verification ispossible due to the ability toinvestigate floating-point models Large team development madeeasy through highlycustomizable tool chain Errors in object code detectedeasily through synchronizationbetween simulations andSILS/PILSImplementation Model(Fixed-point)Model Guideline Check (SLModel Coverage Test (SLVTest Case Auto-Generation(SLDV)Report Auto-Generation(Report Generator)Source CodeSILS/PILS (EC)Runtime ErrorIdentification(Polyspace)Object Code27

Verification and Validation Solutions for High Integrity Systems Tiffany Liang Application Engineer . Requirement Model Test Simulink Verification & Validation Clarification of effects of requirement changes . Auto-Generate Test Cases Property Proving (Formal Methods) V&V Spec Reqmt Spec Controller Model