| 题名 | SRL→Radl生成系统及其相关理论研究 |
| 作者 | 王昌晶 |
| 学位类别 | 博士 |
| 答辩日期 | 2010-09 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 北京 |
| 导师 | 薛锦云 |
| 关键词 | 结构化需求语言 形式化软件规约 生成系统 范畴论 规约相对正确性 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 形式化软件规约技术便于软件系统原型、分析、验证与最终的实现，是保证软件质量和提高软件生产率非常有用和重要的手段。但是形式化规约的获取是一项相当困难的任务，因此通过自动化转换获取形式化规约就显得尤为必要，这已经成为需求工程的重要问题之一。在形式化规约的获取任务中,另一个重要问题是形式化规约的正确性, 即给定一个问题需求，往往可以获取多种不同形式的形式化规约，如何证明这些不同形式规约正确。本文的研究目标是针对问题需求自动化转换为形式化规约与形式化规约正确性这两个重要问题，一是研究从结构化需求语言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平台转换为可执行程序，通过测试已经得到确认。为了支持该方法，进一步提出了扩展的逻辑系统和辅助证明算法。 |
| 英文摘要 | 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 theory. And 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 representation、highly 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: category、sum(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. |
| 语种 | 中文 |
| 公开日期 | 2012-06-20 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/14540]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _学位论文 |
| 推荐引用方式 GB/T 7714 | 王昌晶. SRL→Radl生成系统及其相关理论研究[D]. 北京. 中国科学院研究生院. 2010. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论