比尔·波特,MathWorks公司
本文介绍了在遵循DO-178C、DO-331、DO-333和DO-330的流程中使用基于模型的设计和形式化方法。MathWorks工具可以用于DO-178C项目的开发和验证阶段。虽然MathWorks工具支持系统和软件的广金宝app泛功能,但是对于在需要认证的嵌入式系统上使用工具,推荐使用有限的子集。金宝app动态仿真模块®,Stateflow®,和Simu金宝applink要求™被用来开发符合软件与DO-331基于模型的开发和验证的设计。金宝appSimulink的报告生成器™用于提供一个设计描述文档和跟踪数据,所要求的DO-331和DO-178C。利用Simulink检查™,Simulink的测试™,Simulink的覆盖™和Simulink设计金宝app验证™进行设计的验证。金宝appSimulink设计验证器使用符合DO-333形式化方法形式分析。MATLAB编码器™,Simu金宝applink的编码器™和嵌入式编码器®被用于开发该系统的源代码。的源代码的验证利用Simulink代码检查™,Polyspace错误查找程序™和Polyspace代码金宝app证明者™执行的。Polyspace代码证明器使用符合DO-333形式化方法形式分析。该可执行的目标代码的验证利用Simulink测试和Simulink覆盖率与处理器在环测试功能结合来执行的。金宝app要为使用这些工具的信用,他们必须DO-330软件工具资质注意事项的指导下,合格。该DO资格工具包提供必要的文件和测试文物,为需要它的工具进行工具资格。