| 符合民机适航标准的形式化方法研究 |
| |
| 引用本文： | 王辉,陈蕾,曹杨华,唐晨.符合民机适航标准的形式化方法研究[J].航空电子技术,2019,50(4):53-59. |
| |
| 作者姓名： | 王辉 陈蕾 曹杨华 唐晨 |
| |
| 作者单位： | 中国航空无线电电子研究所, 上海200241;中国航空无线电电子研究所, 上海200241;中国航空无线电电子研究所, 上海200241;中国航空无线电电子研究所, 上海200241 |
| |
| 摘 要： | 描述了形式化方法的定义、目的、作用和软件开发流程。以发动机仪表盘显示布局风格需求为例,通过四变量形式化方法对需求进行形式化建模,通过形式化分析证明模型的完备性和一致性。以发动机油量周期计算需求为例,通过Event-B形式化方法对需求进行形式化建模,通过形式化分析发现需求模型的缺陷。对民机适航标准形式化方法相关的三份补充文件进行了解读,对采用形式化方法进行民机软件开发具有指导意义。
|
| 关 键 词： | 形式化方法 形式化模型 形式化分析 四变量模型 Event-B |
| 收稿时间： | 2019/5/17 0:00:00 |
Research on Formal Method Complying to Civil Standards of Airworthiness |
| |
| WANG Hui,CHEN-Lei,CAO-Yanghu,TANG-Chen.Research on Formal Method Complying to Civil Standards of Airworthiness[J].Avionics Technology,2019,50(4):53-59. |
| |
| Authors: | WANG Hui CHEN-Lei CAO-Yanghu TANG-Chen |
| |
| Institution: | China National Aeronautical Radio Electronics Research Institute,Shanghai 200241,China |
| |
| Abstract: | The definition, purpose, effect and development process of formal method are presented. Taking the layout of engine indicator display requirement as an example, formal model is established by four variable models. Formal analysis is implemented on formal model to prove the completeness and consistency of requirements. Taking the periodic calculation of engine fuel requirement as an example, formal model is established by Event-B, and formal analysis is implemented on formal model to find defects of requirements. Three supplemental documents pertaining to formal method of civil airborne airworthiness standard are interpreted, which can serve as guidance for the use of formal method in the development of civil airborne software. |
| |
| Keywords: | formal method formal model formal analysis four variable model event-B |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《航空电子技术》浏览原始摘要信息 |
| 点击此处可从《航空电子技术》下载免费的PDF全文 |
|
