中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Subject: Computer Science (provided by Thomson Reuters)
Title:
Radl 形式规格说明相对正确性研究
Alternative Title: research on relative correctness of radl formal specification
Author: Wang Changjing ; Xue Jinyun
Keyword: 形式规格说明 ; 相对正确性 ; 确认 ; 扩展的逻辑系统 ; 辅助证明算法
Source: Journal of Software
Issued Date: 2013
Volume: 24, Issue:4
Indexed Type: CSCD
Department: 王昌晶 中国科学院软件研究所 计算机科学国家重点实验室;;江西省高性能计算技术重点实验室 北京 100190 中国. 薛锦云 中国科学院软件研究所 计算机科学国家重点实验室;;江西省高性能计算技术重点实验室 北京 100190 中国.
Sponsorship: 国家自然科学基金重大国际(地区)合作与交流项目; 国家自然科学基金; 江西省自然科学青年科学基金
Abstract: 在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证 这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题 .提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明S_i 等价来实现,而S_i使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法. 使用Radl 语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl 形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.
English Abstract: During the task of acquiring formal specification, an important problem is verifing the correctness of acquired formal specification. In other words, given a problem requirement P, a variety of formal specifications will be acquired, but how to verify the correctness of them all? The different nature of the non- (semi-) formal of problem requirement and formal of specification makes it a challenging software problem and requirement for engineering. This paper proposes a formal derivation method to verify the relative correctness of different forms of Radl specifications corresponding same problem. It achieves this through a proof of the equivalencyamong different forms of Radl specifications and a certain formal specification Si, which is straightforward to the problem requirement. Si is converted into an execute program using PAR method and PAR platform, and is validated by test. In order to support the method, the study further put forth an extended logic system and aided certified algorithm. This paper uses Radl as formal specification language and elaborates the method using two typical examples in the domains of sort and search, combinational optimization. Practical effects manifest not only can effectively verify relatively correctness of Radl specification, but also has well extendibility. The method has potential theory significance and application value in research areas of formal specifications correctness verification, algorithms optimization and programs equivalency proof.
Language: 中文
Citation statistics:
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/15674
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Wang Changjing,Xue Jinyun. Radl 形式规格说明相对正确性研究[J]. Journal of Software,2013-01-01,24(4).
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Wang Changjing]'s Articles
[Xue Jinyun]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Wang Changjing]‘s Articles
[Xue Jinyun]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace