论文部分内容阅读
在软件生命周期中,软件需求分析占有非常重要的地位。需求阶段隐藏的缺陷为安全关键软件的高可靠性埋下巨大的隐患。为了在需求阶段发现和修正隐藏的缺陷,本文提出了一种基于形式化方法的需求缺陷挖掘框架,通过形式化方法对系统的状态和行为进行建模和精化,并通过Rodin平台进行数学推理证明,为安全关键软件的质量提供科学的保障。