基于需求的形式化建模与验证方法研究

• 作者: 曹子宁 李勇
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 形式化方法 RSML-e 模型检测 NuSMV
• 年，卷（期）: 2017,（6）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 7-10
• 页数: 4页
• 分类号: TP31
• 字数: 2943字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2017.06.002

摘要

软件开发过程中需求阶段的错误比设计或实现阶段所引入的错误对系统的安全性与可靠性有更大的影响.为了能够在早期发现错误,降低开发成本,精确、简明地验证和规范软件系统和性质,在模型的形式化开发方法和模型检测的自动验证技术的研究基础上,提出了一种基于需求的形式化建模与验证的框架.运用基于四变量模型的需求状态机语言RSML-e建立了形式化模型,并给出了形式化的转换规则,将RSML-e模型转换为模型检测器NuSMV的输入模型,并进行了检测,建立起了一套整体的形式化开发框架,并以航空电子系统特定实例进行了建模与验证.验证结果表明,已建航电系统模型的安全性和可靠性是有效的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李勇	南京航空航天大学计算机科学与技术学院	142	1840	21.0	37.0
2	曹子宁	南京航空航天大学计算机科学与技术学院	25	200	8.0	13.0