基于需求的形式化建模与验证方法研究李勇,曹子宁南京航空航天大学计算机科学与技术学院,
日期:2019.11.18 点击数:756
【类型】期刊
【刊名】计算机技术与发展
【关键词】 模型检测,E,RSML,Nu,SMV,形式化方法
【摘要】软件开发过程中需求阶段的错误比设计或实现阶段所引入的错误对系统的安全性与可靠性有更大的影响。为了能够在早期发现错误,降低开发成本,精确、简明地验证和规范软件系统和性质,在模型的形式化开发方法和模型检测的自动验证技术的研究基础上,提出了一种基于需求的形式化建模与验证的框架。运用基于四变量模型的需求状态机语言RSML-e建立了形式化模型,并给出了形式化的转换规则,将RSML-e模型转换为模型检测器Nu SMV的输入模型,并进行了检测,建立起了一套整体的形式化开发框架,并以航空电子系统特定实例进行了建模与验证。验证结果表明,已建航电系统模型的安全性和可靠性是有效的,为进一步开发可靠安全的系统奠定了基础。
【年份】2019
【作者单位】南京航空航天大学计算机科学与技术学院
【期号】6
相关文章
- 1、基于需求的形式化建模与验证方法研究李勇,曹子宁南京航空航天大学计算机科学与技术学院, 作者:李勇,曹子宁 年份:2017
- 2、基于严肃游戏的航空理论培训技术研究 作者:逯鹏,刘虎 年份:2016
- 3、一种基于AADL的航空电子系统仿真和验证技术 作者:李铁颖,王科翔,戴苏榕, 年份:2020
- 4、一种航空电子系统体系结构错误行为验证方法 作者:丁明,张书玲,张琛, 年份:2019
- 5、综合模块化航空电子系统安全分析的模型检测方法 作者:邝安玄,马超,王佳明, 年份:2023
- 6、航空公司與旅行社電子商務e-B2B2C運作模式之研究-以C公司為例 作者:胡鴻鈞 年份:2016