基于Why3的形式验证工具实现及ARINC653案例验证

摘要

近年来,随着对于安全关键类软件系统研发的要求不断提高,形式化方法被越来越多的应用于软件系统研发过程中.使用形式化方法依赖形式化语言及其对应的形式验证工具,Why3语言作为形式化语言的一种,因其特性比较符合安全关键类软件系统的形式化验证,正在越来越多的被使用.由于当前Why3缺乏相关整合的形式验证工具,使Why3语言的使用难度增加,所以需要实现一种基于Why3的形式验证工具.本文主要阐述了基于形式化语言Why3的形式验证工具的实现,并使用实现的工具对于ARINC 653标准中的一个案例进行验证.文章首先进行了形式化方法及语言的相关介绍,然后阐述了基于Why3的形式验证工具的实现,最后描述了使用实现的工具对ARINC 653标准中的一个案例进行验证的过程.