摘要:
在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML-e语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML-e模型转化成NuSMV 2模型的方法,并用NuSMV 2对模型的属性进行验证。针对一个真实综合航电系统中的自动飞行控制系统GFC700进行分析验证,实验结果表明,该方法对实际系统的安全性分析具有可行性。
胡军,张维珺,李宛倩. 面向需求的安全关键系统形式化建模与验证方法研究[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.