V&V 。验证Verification vs.确认Validation -验证：Design=Specification? ·保证设计是正确的和完备的 -正确：指精确地实现了SPEC定义的功能、性能等要求 -完备性：描述与所有输入相关的输出 -确认：Design==Requirement? ·形式化验证(Formal verification) 一困难：仅适合于小的设计，或验证某些关键的属性 。 模拟(Simulation)与测试(Testing) 一大多数情况下都采用这种方法 -仅增加了正确性和完备性的可信度 llxx@ustc.edu.cn 6/71
V&V • 验证Verification vs. 确认Validation – 验证：Design == Specification？ • 保证设计是正确的和完备的 – 正确：指精确地实现了SPEC定义的功能、性能等要求 – 完备性：描述与所有输入相关的输出 – 确认： Design == Requirement？ llxx@ustc.edu.cn 6/71 – 确认： Design == Requirement？ • 形式化验证（Formal verification） – 困难：仅适合于小的设计，或验证某些关键的属性 • 模拟(Simulation)与测试（Testing） – 大多数情况下都采用这种方法 – 仅增加了正确性和完备性的可信度
Verification/Validation/Test USTC Verification Testing Validation It focuses on the Hardware It focuses on the correctness of the Revlews Integration functionality of the algorithm,its outputs Fault. product in the real analysis,and SILtest inJection environment according consistency in context Walkthroughs test Uaer to the user of the design Software PiL test HIL Test system Inspection requirements using specifications using Integration Acceptance actual system test iterative test and System test Simulations test components analysis procedures goal simulators and testing for product quality Model analyels procedures for quality improvement checking/ control Static analysls Prototyping Inspectlon llxx@ustc.edu.cn 7/71
Verification/Validation/Test llxx@ustc.edu.cn 7/71
“Y-Chart”Approach for Model--Based Analysis Applications,Platform,Allocation Application Platform Model Model Applic.Constraints Resources QoS .Environment Params .Capacity,speed.etc. .Quality Requirements Reliability(avallabillty .Design Constraints fault tolerance,etc.) Allocation Alloc.Information put Files for .Applic.to Platform Analysis mapping .Allocation-specific properties Analysis Tools Analysis Results Specification of Non-Functional Properties! Generated Code
“Y-Chart” Approach for Model-Based Analysis • Applications，Platform，Allocation
Collaborative Environments CASE Tool Model Checking Code Generation 44 Requirements Manag. Common Repository Analyze Build Code Validate Requirem. Verify Design Integration of V&V Information Reliability Analysis Schedulability Analysis WCET Analysis Performance Simulation
Collaborative Environments
内容提要 Modeling Design Analysis ·系统规约、建模、实现、分析方法：ABC -CBD:分治，结构 -MBD:抽象，分析 Integrate Models to DESIGN-BUILD-VALIDATE-VERIFY 。可视化模型语言 -变迁系统：FSM/HCFSM,Timed Automata -数据流系统：CDFG,数据流进程网络(KPN,SDF) ·应用与工具 到 ·Peter Marwedel,.TU Dortmund教授 战入式系统设计一入式 信息物理系统基础■ -《嵌入式系统设计，嵌入式CPS系统基础》，第2版2011 -第二章：规范与建模 llxx@ustc.edu.cn
内容提要 • 系统规约、建模、实现、分析方法：ABC – CBD：分治，结构 – MBD：抽象，分析 • Integrate Models to DESIGN-BUILD-VALIDATE-VERIFY • 可视化模型语言 llxx@ustc.edu.cn 10/71 – 变迁系统：FSM/HCFSM，Timed Automata – 数据流系统：CDFG，数据流进程网络（KPN，SDF） • 应用与工具 • Peter Marwedel，TU Dortmund教授 – 《嵌入式系统设计·嵌入式CPS系统基础》，第2版2011 – 第二章：规范与建模