模型验证_代码生成_硬件在环.pdf

模型验证、代码生成及硬件在环 董淑成 © 2013 The MathWorks, Inc. 1 模型验证活动 © 2013 The MathWorks, Inc. 2 基于模型设计的模型验证  验证活动及负责人 • 模型复杂度检查 • 建模标准检查 模型开发者 • 形式化方法验证 • 模型评审 开发团队 • 形式化方法验证 • 功能测试及模型更新 模型开发者或 • 形式化方法验证（可能包含属性证明） 独立测试者 注：每个验证活动之后都可以会更新模型 3 模型验证之复杂度检查  低复杂度是高完整性系统软件开发的基本要求  复杂度测量的两种方式 – Model Advisor – 圈复杂度 4 建模规范检查  符合建模规范 – 排除低级错误 – 团队统一建模风格，便于评审和维护  实现方式 – 制定建模规范 – 设计或者选择合理的检查项 – 创建Model Advisor检查集 5 形式化方法验证  检查逻辑错误 – 检查模型中是否有死逻辑 和不能满足覆盖率要求的 逻辑  检查数据错误 – 检查数据被零除、溢出等 错误 6 模型评审  评审建模中可能引入的错误  评审设计是否符合需求 – 需求-模型的双向链接  评审设计变更是否符合需求变更 – 模型比较功能 7 功能测试  单元模块的功能测试 – 功能需求被正确实现 – 测试覆盖率符合要求  需求覆盖率  结构覆盖率  组件级功能测试 – 模块间数据接口的一致性 – 模块间调用关系  系统级功能测试 – 测试模型的系统级功能 – 依赖于被控对象模型 8 形式化方法验证  避免模型经过评审、功能测试之后在更新过程中引入新 的逻辑错误和数据错误 – 检查逻辑错误  Simulink Design Verifier – 检查数据错误  Simulink Design Verifier  属性证明 – 证明模型中