Radl形式规格说明相对正确性研究

CORC > 软件研究所 > 软件所图书馆 > 期刊论文

	Radl形式规格说明相对正确性研究
	王昌晶 ; 薛锦云
刊名	软件学报
	2013
卷号	24 期号:4 页码:715-729
关键词	形式规格说明相对正确性确认扩展的逻辑系统辅助证明算法
ISSN号	1000-9825
其他题名	research on relative correctness of radl formal specification
中文摘要	在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.
收录类别	CNKI ; WANFANG
资助信息	国家自然科学基金重大国际(地区)合作与交流项目(61020106009)\|国家自然科学基金(61272075)\|江西省自然科学青年科学基金(201222BAB211030)
语种	中文
公开日期	2013-09-17
内容类型	期刊论文
源URL	[http://ir.iscas.ac.cn/handle/311060/15494]
专题	软件研究所_软件所图书馆_期刊论文
推荐引用方式 GB/T 7714	王昌晶,薛锦云. Radl形式规格说明相对正确性研究[J]. 软件学报,2013,24(4):715-729.
APA	王昌晶,&薛锦云.(2013).Radl形式规格说明相对正确性研究.软件学报,24(4),715-729.
MLA	王昌晶,et al."Radl形式规格说明相对正确性研究".软件学报 24.4(2013):715-729.