面向需求的安全关键系统形式化建模与验证方法研究

计算机工程与科学

面向需求的安全关键系统形式化建模与验证方法研究

胡军,张维珺,李宛倩

(南京航空航天大学计算机科学与技术学院,江苏南京 211100)

收稿日期:2018-10-29 修回日期:2019-02-27 出版日期:2019-08-25 发布日期:2019-08-25
基金资助:
南京航空航天大学研究生创新基地（实验室）开放基金（kfjj20171611）（中央高校基本科研业务费专项资金）；国家重点基础研究发展计划-973计划（2014CB744903）

A requirement oriented formal modeling and

verification method for safety critical systems

HU Jun,ZHANG Wei-jun,LI Wan-qian

(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211100,China)

Received:2018-10-29 Revised:2019-02-27 Online:2019-08-25 Published:2019-08-25

摘要/Abstract

摘要：

在安全关键系统领域中，明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证，使用RSML-e语言对自动飞行控制系统（AFCS）需求进行建模，提出一种将RSML-e模型转化成NuSMV 2模型的方法，并用NuSMV 2对模型的属性进行验证。针对一个真实综合航电系统中的自动飞行控制系统GFC700进行分析验证，实验结果表明，该方法对实际系统的安全性分析具有可行性。

关键词: MBSE, 自动飞行控制系统（AFCS）, 形式化验证, RSML-e , NuSMV, 模型转换

Abstract:

In the field of safety-critical systems, explicit requirements for the system are essential. We use model-based system engineering idea to model and verify the automatic flight control system (AFCS) based on system requirements. We employ the RSML-e language to model the requirements of the AFCS , propose a method to transform the RSML-e model to NuSMV 2 model, and use the NuSMV 2 to verify the properties of the requirement model. Taking a digital AFCS-GFC700 as an example, we analyze and verify the model. Experimental results show that the method is feasible for the safety analysis of actual systems.

Key words:

MBSE, automaticflight control system (AFCS), formal verification, RSML-e, NuSMV, model transformation

胡军,张维珺,李宛倩. 面向需求的安全关键系统形式化建模与验证方法研究[J]. 计算机工程与科学.

HU Jun,ZHANG Wei-jun,LI Wan-qian.

A requirement oriented formal modeling and

verification method for safety critical systems

[J]. Computer Engineering & Science.

[1]	刘永梅, 王国辉, 关永, 张景芝, 施智平, 董璐. 格林定理的形式化及其初步应用[J]. 计算机工程与科学, 2023, 45(07): 1178-1187.
[2]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[3]	马燕燕1，杨志斌1,2，江国华1. 一种SysML模型到AADL模型的自动转换方法[J]. 计算机工程与科学, 2020, 42(03): 456-466.
[4]	张建民，黎铁军，马柯帆，肖立权. 基于一阶逻辑的可满足求解方法研究进展[J]. 计算机工程与科学, 2019, 41(12): 2119-2126.
[5]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[6]	程亦涵，黄志球，阚双龙. 一种结合AADL和IMC的系统可靠性建模方法[J]. J4, 2015, 37(08): 1517-1524.
[7]	白海洋，李静，赵娜. 基于时间自动机的嵌入式软件模型可调度性验证[J]. J4, 2013, 35(3): 121-127.
[8]	朱梅霞. MARTE顺序图到CCSL模型的转换[J]. J4, 2013, 35(10): 172-180.
[9]	任洪敏，刘晋. 基于行为协议的构件替换性分析[J]. J4, 2012, 34(12): 74-80.
[10]	曾一，王健，洪媛，周欣，蔡森虎. 一种支持MDA的UML类图到RDB模型的转换方法[J]. J4, 2010, 32(4): 67-70.
[11]	刘哲,吴健. 基于本体规则的模型转换的研究[J]. J4, 2010, 32(4): 75-78.
[12]	曾一, 王艳丽, 洪媛, 王健, 刘引. 一种B语言描述的需求模型到PIM的转换方法[J]. J4, 2010, 32(3): 85-88.
[13]	王俐莉王元元张兴元. 命题演算形式系统在Isabelle／HOL中的形式化[J]. J4, 2008, 30(10): 67-68.
[14]	王学斌吴泉源史殿习. 模型驱动架构中的模型转换方法[J]. J4, 2006, 28(11): 133-135.
[15]	周倜李梦君刘万伟李舟军. 安全协议的进程代数规约到逻辑程序的自动转换[J]. J4, 2006, 28(1): 22-24.