计算机工程2017，Vol.43Issue(6)：19-23,29,6.DOI:10.3969/j.issn.1000-3428.2017.06.003
Spark环境下基于SMT的分布式限界模型检测
SMT-based Distributed Bounded Model Checking in Spark
摘要
Abstract
The credibility of program verification results and the verification efficiency in Satisfiablity Modulo Theories (SMT)-based bounded model checking are influenced greatly by bounds.However,the traditional serial checking method cannot validate under the conditions of too large bounds because of the limitation of handling performance and memory in a single machine.In order to solve this problem,this paper proposes a SMT-based distributed BMC method in Spark.First of all,the LLVM Intermediate Representation (LLVM-IR) translated from the source program is converted into Spark built-in data structure Pair Resilient Distributed Dataset(RDD).Afterwards,the Pair RDD is converted into Verification Conditions RDD(VCs RDD) which is then converted into SMT-LIB with the proposed MapReduce algorithm.In the end,the proposed method utilizes SMT solver for verification with the SMT-LIB.Experimental results indicate that,compared with the traditional serial checking method,the proposed method improves not only the bounds of the validation process and the correctness of the verification results,but also the speed of verification for the program with higher complexity under the same bound.关键词
软件验证/限界模型检测/弹性分布式数据集/可满足性模理论求解器/Spark框架Key words
software verification/Bounded Model Checking (BMC)/Resilient Distributed Dataset(RDD)/Satisfiablity Modulo Theories (SMT) solver/Spark framework分类
信息技术与安全科学引用本文复制引用
任胜兵,张健威,吴斌,王志健..Spark环境下基于SMT的分布式限界模型检测[J].计算机工程,2017,43(6):19-23,29,6.基金项目
国家自然科学基金面上项目(61272151) （61272151）
中南大学自主探索创新项目(2016zzts373). （2016zzts373）
