| Title: | Radl形式规格说明相对正确性研究 |
| Alternative Title: | research on relative correctness of radl formal specification
|
| Author: | 王昌晶
; 薛锦云
|
| Keyword: | 形式规格说明
; 相对正确性
; 确认
; 扩展的逻辑系统
; 辅助证明算法
|
| Source: | 软件学报
|
| Issued Date: | 2013
|
| Volume: | 24, Issue:4, Pages:715-729 | | Indexed Type: | CNKI
; WANFANG
|
| Department: | 计算机科学国家重点实验室(中国科学院软件研究所);江西师范大学省高性能计算技术重点实验室;中国科学院研究生院;江西师范大学计算机信息工程学院;
|
| Sponsorship: | 国家自然科学基金重大国际(地区)合作与交流项目(61020106009)|国家自然科学基金(61272075)|江西省自然科学青年科学基金(201222BAB211030)
|
| Abstract: | 在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值. |
| Language: | 中文
|
| Content Type: | 期刊论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/15494
|
| Appears in Collections: | 软件所图书馆_期刊论文
|
|
There are no files associated with this item.
|
| Recommended Citation: | |
王昌晶,薛锦云. Radl形式规格说明相对正确性研究[J]. 软件学报,2013-01-01,24(4):715-729.
|
|
|
