文献类型：期刊文献

中文题名：一种用于循环程序形式化验证的划分归纳方法

英文题名：A Partition Induction for the Formal Verification of Loop Programs

作者：钟杨[1];宋国新[1];计春雷[1,2]

机构：[1]华东理工大学信息科学与工程学院,上海200237;[2]上海电机学院,上海200240

年份：2008

卷号：34

期号：6

起止页码：834

中文期刊名：华东理工大学学报（自然科学版）

外文期刊名：Journal of East China University of Science and Technology

收录：CSTPCD;;EI(收录号：20090611900224);Scopus;北大核心:【北大核心2004】；CSCD:【CSCD2011_2012】；

基金：国家自然科学基金(60473055)

语种：中文

中文关键词：软件可靠性;形式化验证;划分算法;划分归纳方法

外文关键词：software reliability; formal verification; partition algorithm; partition induction

摘要：为了提高软件的可靠性,人们一直在形式化验证和软件测试两个方面进行不懈的努力。本文利用划分测试中的自动分割替代技术,针对循环程序的输入域,提出了一种划分算法,并在此算法的结果上建立一种划分归纳方法,它能简化循环程序的形式化验证过程。
In order to improve software reliability, an unremitting effort has been made on researching fields of formal verification and software test. By using the automatic partition technique in partition test, this paper presents a partition algorithm and constructs a partition induction based on the results that the algorithm generates. This partition induction can simplify the process of formal verification on a loop procedure.