主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
王昌晶,薛锦云.Radl 形式规格说明相对正确性研究.软件学报,2013,24(4):715-729
Radl 形式规格说明相对正确性研究
Research on Relative Correctness of Radl Formal Specification
投稿时间:2011-06-17  修订日期:2011-11-02
DOI:10.3724/SP.J.1001.2013.04260
中文关键词:  形式规格说明  相对正确性  确认  扩展的逻辑系统  辅助证明算法
英文关键词:formal specification  relative correctness  validation  extended logic system  aided certified algorithm
基金项目:国家自然科学基金重大国际(地区)合作与交流项目(61020106009); 国家自然科学基金(61272075); 江西省自然科学青年科学基金(201222BAB211030)
作者单位E-mail
王昌晶 计算机科学国家重点实验室(中国科学院 软件研究所, 北京 100190
江西师范大学 省高性能计算技术重点实验室, 江西 南昌 330022
中国科学院 研究生院, 北京 100190
江西师范大学 计算机信息工程学院, 江西 南昌 330022 
wcj771006@163.com 
薛锦云 计算机科学国家重点实验室(中国科学院 软件研究所, 北京 100190
江西师范大学 省高性能计算技术重点实验室, 江西 南昌 330022 
 
摘要点击次数: 2226
全文下载次数: 2355
中文摘要:
      在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR 方法和PAR 平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl 语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl 形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.
英文摘要:
      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 equivalency among 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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利