点击次数：

所属单位：电子信息工程学院

发表刊物：计算机技术与发展

关键字：形式化方法;RSML-e;模型检测;NuSMV;

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

是否译文：否

发表时间：2017-04-28

合写作者：曹子宁

通讯作者：李勇