符合民机适航标准的形式化方法研究

符合民机适航标准的形式化方法研究

论文摘要

描述了形式化方法的定义、目的、作用和软件开发流程。以发动机仪表盘显示布局风格需求为例,通过四变量形式化方法对需求进行形式化建模,通过形式化分析证明模型的完备性和一致性。以发动机油量周期计算需求为例,通过Event-B形式化方法对需求进行形式化建模,通过形式化分析发现需求模型的缺陷。对民机适航标准形式化方法相关的三份补充文件进行了解读,对采用形式化方法进行民机软件开发具有指导意义。

论文目录

  • 0 引言
  • 1 形式化方法综述
  •   1.1 形式化方法定义
  •   1.2 形式化方法的目的
  •   1.3 形式化方法的作用
  •   1.4 形式化方法的软件开发流程
  •     1.4.1 形式化建模
  •     1.4.2 形式化分析
  •     1.4.3 程序求精
  • 2 形式化方法实践
  •   2.1 四变量形式化方法实践
  •   2.2 Event-B形式化方法实践
  • 3 形式化方法的民机适航标准符合性考虑
  •   3.1 DO-330标准[2]
  •   3.2 DO-331标准新增目标
  •     3.2.1 软件开发过程
  •     3.2.2 软件需求过程输出的验证
  •     3.2.3 软件设计过程输出的验证
  •     3.2.4 软件验证过程结果的验证
  •   3.3 DO-333标准新增目标[4]
  •     3.3.1 软件需求、软件设计、软件编码和集成过程输出的验证
  •     3.3.2 软件验证过程输出结果的验证
  • 4 结束语
  • 文章来源

    类型: 期刊论文

    作者: 王辉,陈蕾,曹杨华,唐晨

    关键词: 形式化方法,形式化模型,形式化分析,四变量模型

    来源: 航空电子技术 2019年04期

    年度: 2019

    分类: 工程科技Ⅱ辑,信息科技

    专业: 航空航天科学与工程,计算机软件及计算机应用

    单位: 中国航空无线电电子研究所

    分类号: V221.91;TP311.52

    页码: 53-59

    总页数: 7

    文件大小: 256K

    下载量: 49

    相关论文文献

    标签:;  ;  ;  ;  

    符合民机适航标准的形式化方法研究
    下载Doc文档

    猜你喜欢