期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到3篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
飞行模式转换的RSML^(-e)到Lustre模型转换与验证方法
1
作者 王智艺 胡军 徐恒 《计算机科学》 北大核心 2025年第12期48-59,共12页
自动飞行系统是现代大型飞机飞行控制的核心系统,飞行导引系统作为自动飞行系统的核心子系统,管理和控制自动飞行系统的模式转换。自动飞行系统的不同飞行阶段本质上是飞行模式的转换,决定了飞机的飞行安全。然而,飞行模式转换具有耦合... 自动飞行系统是现代大型飞机飞行控制的核心系统,飞行导引系统作为自动飞行系统的核心子系统,管理和控制自动飞行系统的模式转换。自动飞行系统的不同飞行阶段本质上是飞行模式的转换,决定了飞机的飞行安全。然而,飞行模式转换具有耦合兼容的多维度复杂静态结构,以及交互合作和过渡切换的多层次模式动态组合的本质特征,因此保证飞行模式转换的正确性至关重要。基于模型驱动的软件建模方法将飞行模式转换需求建模为半形式化模型或形式化模型,从而分析和验证模型满足的性质。现有方法面临两方面挑战:1)自然语言需求到半形式化需求模型的建模,大多为手工建模,且不同建模语言建立的需求模型之间存在差异;2)半形式化需求模型无法直接进行模型检验,需将其转换为模型检验工具的输入模型,且不同的验证工具的验证效率也存在差异。为此,基于自动飞行模式转换的RSML^(-e)需求模型,提出一种将RSML^(-e)模型转换为Lustre同步数据流语言的系统性方法。首先,从数据类型、变量、逻辑短语、AND-OR表、宏等多个维度构建映射规则,将RSML^(-e)模型中元素逐一转换为Lustre同步数据流语言所支持的形式,并在描述安全性质时对变量的数量进行缩减;其次,模型转换后,将转换所得的Lustre模型及安全性质输入Jkind模型检验工具进行验证,基于Jkind模型检验工具内置的多种优化技术,较好地缓解了模型验证过程中状态空间爆炸的问题,实现了对大规模模型的高效验证;最终,通过该流程成功验证了自动飞行系统模式转换需求相关的安全性质,确保系统在各类工况下运行的可靠性。 展开更多
关键词 形式化验证 RSML^(-e) LUSTRE 模型转换 安全性 自动飞行系统
在线阅读 下载PDF
面向需求的安全关键系统形式化建模与验证方法研究 被引量：4
2
作者 胡军 张维珺 李宛倩 《计算机工程与科学》 CSCD 北大核心 2019年第8期1426-1433,共8页
在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML-e语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML-e模型转化成NuSMV... 在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML-e语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML-e模型转化成NuSMV2模型的方法,并用NuSMV2对模型的属性进行验证。针对一个真实综合航电系统中的自动飞行控制系统GFC700进行分析验证,实验结果表明,该方法对实际系统的安全性分析具有可行性。 展开更多
关键词 MBSE 自动飞行控制系统(AFCS) 形式化验证 rsml-e NUSMV 模型转换
在线阅读 下载PDF
基于需求的形式化建模与验证方法研究 被引量：4
3
作者 李勇 曹子宁 《计算机技术与发展》 2017年第6期7-10,共4页
软件开发过程中需求阶段的错误比设计或实现阶段所引入的错误对系统的安全性与可靠性有更大的影响。为了能够在早期发现错误,降低开发成本,精确、简明地验证和规范软件系统和性质,在模型的形式化开发方法和模型检测的自动验证技术的研... 软件开发过程中需求阶段的错误比设计或实现阶段所引入的错误对系统的安全性与可靠性有更大的影响。为了能够在早期发现错误,降低开发成本,精确、简明地验证和规范软件系统和性质,在模型的形式化开发方法和模型检测的自动验证技术的研究基础上,提出了一种基于需求的形式化建模与验证的框架。运用基于四变量模型的需求状态机语言RSML^(-e)建立了形式化模型,并给出了形式化的转换规则,将RSML^(-e)模型转换为模型检测器NuSMV的输入模型,并进行了检测,建立起了一套整体的形式化开发框架,并以航空电子系统特定实例进行了建模与验证。验证结果表明,已建航电系统模型的安全性和可靠性是有效的。 展开更多
关键词 形式化方法 RSML^-e 模型检测 NUSMV
在线阅读 下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部