Overview of MathWorks

Similar documents
PowerPoint Presentation

模型验证最佳实践

Presentation Title


PowerPoint プレゼンテーション

Presentation Title

目次 

会 议 组 织 研 讨 会 主 席 : 周 巢 尘 院 士 ( 中 国 科 学 院 软 件 研 究 所 ) 程 序 委 员 会 主 席 : 段 振 华 教 授 ( 西 安 电 子 科 技 大 学 ) 董 云 卫 教 授 ( 西 北 工 业 大 学 ) 工 业 专 题 主 席 : 叶 宏 研 究 员

使用Polyspace进行软件代码错误检查和运行期错误证明

2014_

PowerPoint 簡報

13 A DSS B DSS C DSS D DSS A. B. C. CPU D. 15 A B Cache C Cache D L0 L1 L2 Cache 16 SMP A B. C D 17 A B. C D A B - C - D

Presentation Title

2/80 2

OOAD PowerDesigner OOAD Applying PowerDesigner CASE Tool in OOAD PowerDesigner CASE Tool PowerDesigner PowerDesigner CASE To

Presentation Title

<4D F736F F F696E74202D20C8EDBCFEBCDCB9B9CAA6D1D0D0DEBDB2D7F92E707074>

資訊系統開發模式

Presentation Title

Presentation Title

892213E006146

小论文草稿2_邓瀚

Microsoft Word - 专论综述1.doc

创业板投资风险提示:本次股票发行后拟在创业板市场上市,该市场具有较高的投资风险

(Electronic Data Interchange) (Executive Information System) (Economic Order Quantity) (Enterprise Resource Planning) (Flexible Manufacture System) (F


epub 79-1

untitled

rz_Newsletter2016_en_ indd

XXX专业本科人才培养方案

epub83-1

ebook204-2

Microsoft PowerPoint ARIS_Platform_en.ppt

<4D F736F F D D36207A BAABCEB0C7BF20B5E7CDF8D4CBD0D B7D6CEF6B5C4BFC9D0D0D0D4BCB0B7BDCABDCCBDCCD62E646F63>

Thesis for the Master degree in Engineering Research on Negative Pressure Wave Simulation and Signal Processing of Fluid-Conveying Pipeline Leak Candi

PowerPoint Presentation

職業安全衛生績效量測技術手冊

IP TCP/IP PC OS µclinux MPEG4 Blackfin DSP MPEG4 IP UDP Winsock I/O DirectShow Filter DirectShow MPEG4 µclinux TCP/IP IP COM, DirectShow I


CH01.indd

Microsoft PowerPoint - Aqua-Sim.pptx

Olav Lundström MicroSCADA Pro Marketing & Sales 2005 ABB - 1-1MRS755673

中华人民共和国水利行业标准(封面).doc

内部资料,注意保密

计 算 机 系 统 应 用 年 第 25 卷 第 1 期 的 编 程 语 言 Giotto [9] 编 写 控 制 程 序, 可 以 方 便 的 控 制 程 序 的 逻 辑 执 行 时 间, 从 而 使 得 任 务 时 间 的 依 赖 关 系

案例正文:(幼圆、小三、加粗)(全文段前与段后0

D C 93 2

the requirements of load - bearing rescue and turning of the large fire engine can be served as an outdoor safety area. 5 The second floor

? MRP MRP 1960 Bill of Material Light and Holland 2000 MRPII MRP MRPII MRP ERP Gartner Group ERP ERP MRP MRP-II APICS 1995 ERP ERP ERP Daven

資訊安全管理系統建置初始工作的研究

Microsoft Word - A doc

<4D F736F F D20312D3120D5D0B9C9CBB5C3F7CAE9A3A8C9EAB1A8B8E5A3A9>

Chapter 24 DC Battery Sizing

mvc

FAQ -PowerDesigner9.5.DOC

f2.eps

LH_Series_Rev2014.pdf

EK-STM32F

1 目 錄 1. 簡 介 一 般 甄 試 程 序 第 一 階 段 的 準 備 第 二 階 段 的 準 備 每 間 學 校 的 面 試 方 式 各 程 序 我 的 做 法 心 得 及 筆 記 結 論..

政府機關_構_資通安全責任等級分級作業規定

m 2, m 2,,,, 20. 5m,, 4. 6 m 2 3, m, 87200m 2,, ( ) Leoadaly 1 C40, 2200mm 2650mm, 30m, 49000kN 71000kN, 193m, 156m,,, 2 1,

豐佳燕.PDF

Wy159.mps

廠 商 攤 位 配 置 圖 ~ 2

untitled

Microsoft PowerPoint - 数据通信-ch1.ppt

2 3. 1,,,.,., CAD,,,. : 1) :, 1,,. ; 2) :,, ; 3) :,; 4) : Fig. 1 Flowchart of generation and application of 3D2digital2building 2 :.. 3 : 1) :,

( CIP ) /. - :, ISBN X G420 CIP (2003) JIAOYU ZHILIANG DUDAO YU PINGJIA : (0898 ) B 3 :

csr_report_2009.pdf

FANUC Power Motion i-MODEL A

Automatic Protocol Conformance Test Generation Based on Model Checking By JI ZHONG HE A dissertation submitted to the graduate faculty in partial fulf

IEC 传输帧格式

untitled

JOURNAL OF EARTHQUAKE ENGINEERING AND ENGINEERING VIBRATION Vol. 31 No. 5 Oct /35 TU3521 P315.

ebook

路演公告.PDF

软 件 工 程 专 业 习 指 南 目 录 一 软 件 工 程 专 业 设 置 背 景 与 发 展 前 景... 3 二 软 件 工 程 专 业 实 践 教 条 件... 4 三 软 件 工 程 专 业 课 程 类 型 及 核 方 式 软 件 工 程 专 业 课 程 类 型...7

(Geographic data or geodata ) 30 (Buelher, K and L. Mckee1996) (Open GIS Consortium OGC) OGC GIS Open GIS OGC (Geography Markup Langu

55

目 录

软件测试(TA07)第一学期考试

FEJC **.pdf

untitled

<4D F736F F D20B1B1BEA9BAA3F6CEBFC6BDF0B8DFBFC6BCBCB9C9B7DDD3D0CFDEB9ABCBBECAD7B4CEB9ABBFAAB7A2D0D0B9C9C6B1D5D0B9C9CBB5C3F7CAE9A3A8C9EAB1A8B8E C4EA35D4C23132C8D5B1A8CBCDA3A92E646F63>

TEEx Transducer User Guide

声 明 本 公 司 及 全 体 董 事 监 事 高 级 管 理 人 员 承 诺 不 存 在 虚 假 记 载 误 导 性 陈 述 或 重 大 遗 漏, 并 对 其 真 实 性 准 确 性 完 整 性 承 担 个 别 和 连 带 的 法 律 责 任 本 公 司 负 责 人 和 主 管 会 计 工 作 的

SDS 1.3

<4D F736F F D20C9CFBAA3BFC6BCBCB4F3D1A7D0C5CFA2D1A7D4BA C4EAC7EFBCBEC8EBD1A7B2A9CABFD7CAB8F1BFBCCAD4CAB5CAA9CFB8D4F22D C8B7B6A8B8E5>

A dissertation for Master s degree Metro Indoor Coverage Systems Analysis And Design Author s Name: Sheng Hailiang speciality: Supervisor:Prof.Li Hui,

藍牙網路在資訊家電的應用


013 機 械 相 關 科 系 畢, 對 銑 削 加 工 中 心 機 有 興 機 器 組 裝 人 員 協 銳 精 密 工 業 股 趣, 具 高 度 工 作 熱 忱 者 份 有 機 械 相 關 科 系 畢, 邏 輯 思 考 能 力 佳, 抗 壓 電 控 設 計 組 裝 人 員 性 高, 肯 接 受 挑

audiogram3 Owners Manual


<4D F736F F D20D5E3BDADD5FDD4AAD6C7BBDBBFC6BCBCB9C9B7DDD3D0CFDEB9ABCBBECAD7B4CEB9ABBFAAB7A2D0D0B9C9C6B1B2A2D4DAB4B4D2B5B0E5C9CFCAD0D5D0B9C9CBB5C3F7CAE9A3A8C9EAB1A8B8E C4EA36D4C23139C8D5B1A8CBCDA3A92E646F63>

OSI OSI 15% 20% OSI OSI ISO International Standard Organization 1984 OSI Open-data System Interface Reference Model OSI OSI OSI OSI ISO Prototype Prot

m 3 m m 84 m m m m m m m

財金資訊-84期.indd

基于Proficy软件平台的大直缝埋弧 焊管生产线MES系统——王东明(初编辑稿-作者修改)

4 115,,. : p { ( x ( t), y ( t) ) x R m, y R n, t = 1,2,, p} (1),, x ( t), y ( t),,: F : R m R n.,m, n, u.,, Sigmoid. :,f Sigmoid,f ( x) = ^y k ( t) =

Transcription:

基于模型设计助力高安全关键系统软件开发 符合行业标准的 MBD 方案及案例解析 于化龙高级项目开发部经理迈斯沃克 ( 软件 ) 北京有限公司 2015 The MathWorks, Inc. 1

内容概要 国内外高安全关键系统开发与验证的趋势 符合行业标准的基于模型设计解决方案 轨道交通行业符合 EN50128 标准项目实践 2

高安全关键系统软件开发面临的挑战 系统复杂度不断增大 开发周期不断缩短 代码量急速增长 软件质量与认证要求 更加严苛的行业标准 更高的安全性考虑 3

基于模型设计已成为高安全关键系统软件开发的趋势 4

意大利 Selex 公司基于模型设计技术历程 http://www.mathworks.com/tagteam/75977_concepts_to_chips_selex_es.pdf 5

意大利 Selex 公司飞行系统 (March 2013) Motor Control MATLAB Simulink Embedded Coder Systems HDL Coder Doppler Radar Software PIL Hardware FIL HIL http://www.mathworks.com/tagteam/75977_concepts_to_chips_selex_es.pdf 6

Alstom Generates Production Code for Safety-Critical Power Converter Control Systems (2004) Challenge Design and implement real-time power conversion and control systems for trams, metros, and railways Solution Use MathWorks tools for Model-Based Design to design, simulate, and automatically generate production code for safety-critical transportation systems Results Development time cut by 50% Defect-free, safety-critical code generated and certified Common language established Link to user story Pendolino tilting train. When Alstom delivered a Pendolino train to Czech Railways, the railway application was the first with automatically generated code to receive TUV certification (for EN 50128) Han Geerligs Alstom 7

Alstom (Nov.2013) 8

基于模型设计的关键在于从仿真到实现 模型 : 只是用做仿真 Simulink 仿真模型 Word 手工文档 C 手写代码 - 设计部门仍然通过手写设计文档来交给软件部门 - 设计部门可能需要维护模型 / 代码 / 文档三套设计 - 软件部门仍然根据文档进行手工编码 - 代码编写存在需求理解偏差, 易引入认为缺陷 Simulink 仿真模型 Simulink 产品模型 C/HDL 自动代码 模型 : 自动生成代码 仿真模型经过配置后可以直接生成代码 设计部门可将仿真模型或者配置好的产品模型交付 软件部门可以对模型进行配置后自动生存代码 通过定制可以实现自动代码与手写代码的自动集成 9

基于模型设计使早期验证成为可能 10

基于模型设计 : 以模型为核心集成设计开发环境 项目管理 Simulink Project 需求管理 Simulink VnV RMI DOORS Integration 知识管理 Simulink VnV Model Advisor Simulink Customized Library 数据管理 Simulink Data Dictionary Simulink Data Inspector Simulink System 系统架构 XML In/Out 硬件集成 Processor In Loop Hardware In Loop 配置管理 Simulink Project SVN/CC Integration 报告生成 MATLAB Report Generator Simulink Report Generator 11

内容概要 国内外高安全关键系统开发与验证的趋势 符合行业标准的基于模型设计解决方案 轨道交通行业符合 EN50128 标准项目实践 12

高安全关键系统相关行业标准 DO-178 (Level A) ISO 26262 ARP4754 & DO-178 Honeywell Aerospace USA Flight Control Systems TRW Germany Electronic parking brake control system Airbus Helicopters Certified flight software IEC 62304 IEC 61508 EN 50128 Weinmann Medical Germany Transport ventilator Alstom Grid UK HDVC Power Systems Alstom France Train Control Systems 13

DO Qualification Kit IEC/ISO Certification Kit >>qualkitdo >>certkitiec 14

15

16

参考流程 Simulink Test, Model coverage (SL V&V), Requirements Trace Interface (SL V&V), Report Generation and Diff (SL RG) Property proving (SLDV) Trace matrix generation (Cert Kit), Code coverage tool integration (Embedded Coder), Structural equivalence (Simulink Code Inspector) Module and Integration testing Model Standards Checks (SL V&V) Reviews and static analysis PIL testing (Embedded Coder), Test generation (SLDV) Prevention of unintended functionality Reviews and static analysis Equivalence testing Polyspace (MISRA) Polyspace Code Prover Textual requirements Executable specification Model used for production code generation Generated code Object code Modeling Simulink / Stateflow / Simulink Fixed Point Code generation Embedded Coder Compilation and linking 17

思考一个问题 : 工程师为什么无法充分利用模型? Simulink 只用于仿真 工程师使用 Simulink 仅用于算法仿真, 并没有将 Simulink 平台作为全流程的开发工具, 关键是仍没有突破自动代码生成的技术和心理障碍, 模型验证更是无从谈起 模型无法在开发中传递 Simulink 模型仿真完成后, 工程师又忙于琐碎的文档和编码工作, 模型无法向下传递, 还没有成为知识传递与积累的载体, 模型也没有实现标准化的设计 开发流程无法自动化 Simulink 提供了建模 / 仿真 / 验证 / 代码生成等一些列工具, 但这些工具都相对独立, 并没有与特定的流程进行集成, 所以导致工程师在使用时没有目标, 或者就不知何时使用 团队协作过于粗放 在团队协作中, 流程的定义相对粗放, 没有规定每一个环节工程师详细的工作职责 / 使用工具 / 输入输出等, 而且如模型验证等环节都是缺失的, 模型没有进入到设计开发流程中 18

从 V 流程到 微 流程 Requirements Design Integration Acceptance 微 流程 解决了设计过程中的实现操作定义, 每个操作都是可执行的, 工程师可以参照它开展工作 模型验证版本库 tpj_projectname.prj prj_starttestproject.m 被测模型 模型验证开始获取项目数据打开项目文件配置测试环境模型规范检查 设定工作路径载入模型数据 Model Advisor 报告 被测模型 模型缺陷检查 Design Verifier 报告 被测模型 模型覆盖率检查 Design Verifier 报告 Code 需求追踪 模型设计 需求 模型缺陷检查模型规范检查 模型功能性验证模型覆盖率验证 需求文档被测模型 需求文档 是 缺陷? 否设计测试模型设计测试用例 ths_model_xxx.mdl tcs_model_xxx.xlsx 需求追踪 代码生成 模型 模型与代码结构一致性验证 目标码功能性验证代码运行时缺陷检查 tru_model_xxx.m 运行测试用例比较测试结果覆盖率 100%? 否 是 trp_model_xxx.doc tcv_model_xxx.cvt trs_model_xxx.mat V 流程 解决了设计过程中主要环节定义, 但没有具体的实现, 工程师无法参照它开展工作 编译 源代码 可执行目标码 代码规范检查 模型与目标码功能一致性验证代码运行时缺陷检查代码覆盖率验证 问题报告 prp_model_xxx.doc tcv_model_xxx.cvt Signal Builder 否 补充测试用例满足覆盖率要求转换测试用例设定期望值结果 100% 是提交全部测试文件下一个模型? 否项目实施结束 是 Signal Builder tcs_model_xxx.xlsx tcs_model_xxx.xlsx ths_model_xxx.mdl trp_model_xxx.doc prp_model_xxx.doc tcv_model_xxx.cvt trs_model_xxx.mat 19

内容概要 国内外高安全关键系统开发与验证的趋势 符合行业标准的基于模型设计解决方案 轨道交通行业符合 EN50128 标准项目实践 20

案例项目背景 欧洲铁路运输管理系统 (ERTMS) Level 2 Radio Block Center (RBC) 系统 项目目标 符合 SIL4 项目的最佳实践 EN50128 标准符合性指导 21

22

基于模型设计 :V 流程 Software requirement s Software development Planning Application Software development Software validation Hardware and Basic Software integration Software architecture and design Software design simulation and analysis Automatic software code testing Software component design Software component design simulation and analysis Automatic software component code testing Automatic code generation and analysis Model-Based Design 23

基于模型设计 : 实施环节 1 软件项目计划 软件需求描述 软件确认 硬件与软件集成 软件架构设计 软件集成设计仿真与验证 自动化软件代码集成测试 软件单元设计 软件单元设计仿真与验证 自动化软件代码单元测试 2 3 5 自动代码生成与分析 4 基于模型设计 24

基于模型设计在项目中的实施 1 2 3 4 5 项目计划 : 基于模型的软件开发项目计划软件设计 : 基于模型的软件架构与单元设计模型验证 : 基于模型的设计仿真与验证代码生成 : 基于模型的自动代码生成与分析代码验证 : 基于模型的代码集成与验证 25

1 基于模型的软件开发项目计划 26

使用 Certification Kit 对流程进行定义 明确定义项目范围 在软件质量保证计划 (SQAP) 中根据 TÜV SÜD for SIL4 批准的流程详细制定项目开发流程 必须详细描述流程的细节并且映射到 EN50128 表格中 27

标准和符合性验证 通过 Model Advisor 中 EN50128 检查项自动验证模型标准的符合性 通过 Polyspace 中 MISRA AC AGG 检查工具自动验证代码标准的符合性 28

使用 Certification Kit 对工具进行认证 对项目建立认证包实例 Certification Kit 针对每个 MATLAB 版本都会进行升级 自动运行工具的测试程序并且生成报告 29

使用 Simulink Project 管理项目 确保工具配置的一致性 通过行为执行的自动化快捷操作确保流程的符合性 在 CM 下保持项目团队的合作 提供完整项目的依赖关系分析 通过自动化脚本实现行为执行的批处理操作 30

2 基于模型的软件架构与单元设计 31

软件架构设计 Software requirements Software requirements specification Software architecture and design Model architecture and specify design Software architecture specification model specification model Verify modelling standard Generate Architecture Spec Software architecture, design and interface specification Specify tests Software and Software/Hardware integration test specification Specify properties Software and Software/Hardware properties specification report Do: manual activity Do: automated activity Modelling Standard Conformance Report Review Review Review Review Software Architecture and Design Verification Report Approve 32

软件架构设计中的开发活动 架构模型限定在应用层软件 开发软件架构描述模型 使用 Simulink 图形化描述模块划分和数据流 使用 MATLAB 描述接口特性 使用富文本注释在模型中描述设计依据和需求 建立模型与需求的追踪 软件架构设计文档通过模型自动生成 33

软件架构设计中的验证活动 描述软件集成测试 软件集成测试用例与需求建立追踪 验证模型规范的符合性 验证测试描述 同级审核 验证软件架构描述 同级审核 34

软件单元设计 Software architecture and design Software architecture specification model Software component design Model algorithms and equations Software component design model specification model Verify modelling standard Generate Component Spec Software component design specification Specify tests Software component test specification Specify properties Software component properties specification report Do: manual activity Do: automated activity Modelling Standard Conformance Report Review Review Review Review Software Architecture and Design Verification Report Approve 35

软件单元设计中的开发活动 开发软件单元描述模型 软件架构模型描述单元接口 根据架构模型中的单元需求开发具体的算法和方程 设计依据包含在模型中的富文本注释中 软件单元需求与模型建立追踪 软件单元描述文档通过模型自动生成 36

软件单元设计中的验证活动 验证软件单元模型 模型规范符合性自动化验证 软件单元描述同级审核 需求追踪型验证 设计鲁棒性验证 设计可测试性验证 详尽验证单元测试描述 软件单元测试描述同级审核 37

3 基于模型的设计仿真与验证 38

Component design testing 模型单元测试 Component design Software component design model Software component test specification Build test harness model Component test harness Simulate and log outputs Record design model structural coverage Software component design structural coverage and test report Software component test cases Specify test I/O values Review Review sw phase specification model report Do: manual activity Do: automated activity Review Software component design test report Approve 39

模型单元测试中的活动 创建测试模型 引用被测设计模型并将其连接到测试输入 比较测试的期望值与模型输出值 启动单元模型的结构覆盖率测量 启动信号信号范围覆盖率测量 执行测试程序 载入测试数据到 MATLA 工作空间 仿真测试模型 统计累积覆盖率并生成报告 审核模型单元测试描述和报告 40

Model integration 模型集成与测试 Component design Architecture and design Software component design model Software architecture specification model Software integration test specification Verify modeling standard Integrate Software integration model Review Review Specify test I/O values Software integration test cases Build test harness model Integration test harness model Simulate and log outputs Software integration test report Review Review Do: manual activity Do: automated activity <name > SW Phase <name > <name > <name > Specification Model Report Software integration verification Report Approve 41

模型集成与测试中的活动 开发 : 将单元模型集成到软件架构模型中 测试 : 创建测试模型 执行测试程序 验证 : 验证集成模型的规范符合性 审核集成模型 审核测试报告 42

4 基于模型的自动代码生成 43

Component implementation 自动代码生成与分析 Component design Software component design model Generate code Software source code and supporting information sw phase specification Verify coding standard MISRA AGC compliance report Review Verify Bug Finder checks Verify Polyspace Code Prover checks Polyspace verification report Review model report Do: manual activity Do: automated activity Software component implementation report Approve 44

自动代码生成 可读性与可追溯性 自动生成具有代码和模型双向链接的报告 提供代码生成指标 通过配置确保 C 代码中的算法结构 45

自动代码分析 使用 Polyspace Bug Finder 验证生成代码与 MISRA 标准的符合性 使用 Polyspace Code Prover 验证生成代码的鲁棒性 46

5 基于模型的代码集成与验证 47

Component code testing 代码单元测试 Component Implementation Component design testing Component source code and supporting information Software component test cases Instrument code and generate exe Fee d Component test harness sw phase specification model Component Code coverage report Measure code coverage Review Software component implementation verification report Approve Component test report Review Measure test result report Do: manual activity Do: automated activity 48

Code integration 代码集成测试 Component implementation Model integration Component source code and supporting information Software integration model Software integration test cases Generate code Integration source code and supporting information Generate exe Feed sw phase specification Verify Polyspace RTE checks Verify coding standard Integration test harness Measure test result model report Do: manual activity Do: automated activity Polyspace verification report MISRA AGC compliance report Integration test report Review Review Review Software component implementation verification report Approve 49

自动化代码测试 使用 Simulink Design Verifier 自动生成背靠背测试用例或正重用基于需求的测试用例 自动化软件在环测试或者处理器在环测试 使用集成的第三方工具 LDRA 统计代码覆盖率 使用 Simulink Data Inspector 比较模型与代码的输出 50

自动化代码测试 51

总结与问题 国内外高安全关键系统开发与验证的趋势 符合行业标准的基于模型设计解决方案 轨道交通行业符合 EN50128 标准项目实践 52