中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
Title:
SRL→Radl生成系统及其相关理论研究
Author: 王昌晶
Issued Date: 2010-09
Supervisor: 薛锦云
Major: 计算机软件与理论
Degree Grantor: 中国科学院研究生院
Place of Degree Grantor: 北京
Degree Level: 博士
Keyword: 结构化需求语言 ; 形式化软件规约 ; 生成系统 ; 范畴论 ; 规约相对正确性
Abstract: 形式化软件规约技术便于软件系统原型、分析、验证与最终的实现,是保证软件质量和提高软件生产率非常有用和重要的手段。但是形式化规约的获取是一项相当困难的任务,因此通过自动化转换获取形式化规约就显得尤为必要,这已经成为需求工程的重要问题之一。在形式化规约的获取任务中,另一个重要问题是形式化规约的正确性即给定一个问题需求,往往可以获取多种不同形式的形式化规约,如何证明这些不同形式规约正确。本文的研究目标是针对问题需求自动化转换为形式化规约与形式化规约正确性这两个重要问题,一是研究从结构化需求语言SRL到形式化规约语言自动生成系统及其高可靠性理论,二是研究形式化规约的相对正确性问题。为了使研究工作与PAR方法及其支撑平台无缝衔接,本文使用Radl语言作为形式化软件规约语言。围绕研究目标,本文的具体研究内容与成果包括:1为了减少或消除自然语言固有的歧义性,设计了一种受控自然语言--结构化需求语言(Structural Requirement Language, 简称SRL)来描述问题需求。该语言词语、句型、语义和语用都受控,便于普通用户使用。具有功能强大、高度数据抽象和可扩充性、支持泛型机制、丰富的语料库、量词结构化等特点。2. 为了描述结构化需求语言SRL与形式化软件规约Radl两个领域不同级别的形式化,并进一步刻画SRL语言与Radl语言之间的转换关系,通过深入分析,提炼出源语言SRL分析规则、目标语言Radl生成规则以及源语言SRL到目标语言Radl转换规则三组规则。使用基于规则的方法,将结构化需求语言SRL通过分析-转换-综合三阶段生成为形式化软件规约Radl。3在基于规则的生成方法指导下,设计并实现了结构化需求语言SRL到形式化软件规约Radl的生成系统SRLtoRadl。使用自然语言处理(Natural Language Processing, 简称NLP)的技术对生成系统SRLtoRadl词法分析、语法分析、语义分析中的诸多难点进行了处理。4.利用范畴论的基本概念:范畴、和(积)、外推(回拉)、余极限(极限)、函子(反变函子)、遗忘函子等,使用范畴论框架逐步的建立了SRLtoRadl生成系统生成过程的语义模型,它是SRLtoRadl生成系统高可靠性的理论基础

5.提出一种基于形式化推导的方法来验证与确认同一问题不同形式规约,这是通过证明不同形式规约与问题需求某个最为直截明了的形式化规约Si等价来达到的,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认。为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法。

English Abstract: Formal software specification techniques facilitate the prototype, analysis, verification and final implementation of software system. The employment of formal specification techniques in software development is very useful and important for improving quality and productivity of software. But formal specification acquisition is a quite difficult task, so the automatic conversion to acquire formal specification is particularly necessary, it has become one of important problem of requirement engineering. Another important problem is the correctness of acquired specification, i.e., given a problem requirement, a variety of formal specifications will be acquired, how to prove them correctness.The research objectives aim to the above two problems about automating conversion from problem requirement into a formal specification and formal specification correctness. This paper studies the automation generation system from Structural Requirement Language(SRL) into formal specification and its high reliablity theoryAnd study the relative correctness of formal specification.To make seamless transition between our research work and PAR method and its Platform, use Radl language as a formal software specification language.Focus on research objective, this paper's research contents and results include:1. In order to reduce or eliminate the inherent ambiguity of natural language, design a controlled natural language- Structural Requirement Language (SRL) to describe the problem requirement. Its words, grammars and structures are limited, easy to use by ordinary users. SRL has the following characteristics: power representationhighly data abstraction and scalableness, supporting generic mechanism, rich corpus, structured quantifiers and so on.2. In order to describe the different level of the formalism between the two domains of SRL and the formal software specification Radl, and further express the conversion relation between SRL language and Radl language. Through deeply analysis, extract the analysis rules of source language SRL, the generation rules of target language Radl and the conversion rules from SRL to Radl. Using rule-based method, convert SRL into Radl by analysis-transformation-synthesis three stages.3. Under the guidance of the rule-based generation method, design and implementation of generation system from SRL to Radl, called SRLtoRadl. Dealing with many difficulties in lexical analysis, syntax analysis, and semantic analysis of the generation system SRLtoRadl by natural language processing (NLP) techniques.4. Using basic concepts of category theory: categorysum(product)pull out(pull back)colimit(limit)functor(opposite functor)forgetful functor and so on, establish the generation process semantic model of SRLtoRadl by category theory framework. It is the theory basis to ensure high reliability of generation system SRLtoRadl.5. Proposing a formal derivation method to verify and validation relative correctness of different forms of Radl specifications corresponding same problem. It achieves by proof the equivalency of different forms of Radl specifications and a certain formal specification, which is straightforward to problem requirement. Convert it into an execute program by PAR method and its platform, then the certain formal specification is validated by rigorous test. For derivation method, further put forward a tailored first-order predicate logic system and auxiliary proof algorithm.
Language: 中文
Content Type: 学位论文
URI: http://ir.iscas.ac.cn/handle/311060/14540
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
2012.6.20+博士论文.pdf(787KB)----限制开放 联系获取全文

Recommended Citation:
王昌晶. SRL→Radl生成系统及其相关理论研究[D]. 北京. 中国科学院研究生院. 2010-09-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[王昌晶]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[王昌晶]‘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-2021  中国科学院软件研究所 - Feedback
Powered by CSpace