关键词:
形式化方法
B方法
需求规格
可靠性
验证
摘要:
伴随着互联网技术的进步,传统的考试手段产生了巨大的变化,它的包容性、分散性和复杂的计算能力突破了传统考试的时空界线。借助遍布于世界各地的因特网,在线考试软件具有安全、客观、公平、便捷、高效等的特性。因而,今后考试的发展方向必然是在线考试。面临软件规模及其复杂程度的不断提高,为了实现软件的社会价值,怎样提高软件的可靠性,如何能保证软件的质量,已经成为软件工程领域研究的一个热门问题。而作为一种高安全性、实时的软件,在线考试软件如果出现问题,具有突然性和爆发性,将会造成不可估计的后果,是人们所不能忍受的,所以在线考试软件具有很高的可靠性要求,对其需求规格验证方法进行研究,有其必要性。形式化方法(Formal Method,FM)是一种采用严谨的数学语言来描述系统性质的技术,B方法是比较典型的形式化方法,它可以支持软件开发的全过程,具备完整的数学理论基础,且拥有完善的支持辅助工具。采用B方法描述在线考试软件的需求规格,可以有效避免需求说明的不确定性,在某种程度上确保需求符合用户需要。本文首先介绍了在线考试软件、软件可靠性和形式化方法的研究现状和发展趋势,从而引出了在线考试软件需求规格形式化和对其可靠性进行研究的必要性。接着,详细描述了该软件的需求,包括功能性需求和非功能性需求,本文重点关注在线考试软件的可靠性需求,因此对其可靠性需求进行了着重阐述。其次,采用B方法对在线考试软件的需求规格进行了形式化描述,确保了需求规格的一致性和无二义性,减少了需求分析阶段可能出现的影响系统可靠性的错误。然后,通过创立其可靠性模型,对在线考试软件的可靠性需求进行描述。最后,对在线考试软件的形式化需求规格进行验证,通过定理证明,确保所实现的软件符合用户需求,从而保证了在线考试软件的高可靠性。