| Radl形式规格说明相对正确性研究 |
| 其他题名 | research on relative correctness of radl formal specification
|
| 王昌晶; 薛锦云
|
| 2013
|
| 发表期刊 | 软件学报
 |
| ISSN | 1000-9825
|
| 卷号 | 24期号:4页码:715-729 |
| 摘要 | 在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值. |
| 收录类别 | CNKI
; WANFANG
|
| 关键词 | 形式规格说明
相对正确性
确认
扩展的逻辑系统
辅助证明算法
|
| 部门归属 | 计算机科学国家重点实验室(中国科学院软件研究所);江西师范大学省高性能计算技术重点实验室;中国科学院研究生院;江西师范大学计算机信息工程学院;
|
| 资助者 | 国家自然科学基金重大国际(地区)合作与交流项目(61020106009)|国家自然科学基金(61272075)|江西省自然科学青年科学基金(201222BAB211030)
|
| 语种 | 中文
|
| 内容类型 | 期刊论文
|
| URI标识 | 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.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论