中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于组件的逐步求精程序设计方法
作者: 郑建丹
答辩日期: 2001
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: XYZ系统 ; 时序逻辑语言 ; 软件体系结构 ; 逐步求精 ; 形式化方法
摘要: 软件体系结构是近年来软件工程界的热门研究领域之一。在软件体系结构设计过程中,经常要碰到的问题是如何从抽象的高层体系结构逐步过渡到底层的体系结构直到最后的实现。这个过渡过程要保证每层过渡的正确性,否则最后得到的可执行程序可能不是最初所想要的目标程序,因此如何对体系结构求精显得尤其重要。这也是本文要致力解决的问题。基于组件的由静态语义向动态语义逐步过渡的程序设计方法从体系结构的基本元素-组件入手,用XYZ/E形式化体系结构,每次的求精都是对组件的求精,而不是整个体系结构,组件的求精就是用组件的动态语义代替组件的静态语义,由于XYZ/E具有可以在统一的框架下描述静态语义和动态语义的特点,从而使系统能够从最初的体系结构设计平滑到最后的可执行程序。求精一致性的验证可以借助于基于Hoare逻辑规则的验证工具XYZ/VERI以及XYZ/E作为时序逻辑语言所具有的对一些程序性质的证明方法。本文首先用时序逻辑语言XYZ/E形式化描述体系结构中的基本组件和连接件以及体系结构风格,说明如何用XYZ/E描述软件体系结构然后在此基础上提出基于组件的由静态语义向动态语义逐步过渡的程序设计方法,将软件体系结构XYZ系统有机的结合起来。这种方法的优点是在统一的框架下描述不同抽象程度的体系结构,使体系结构的第一步求精能够平滑的过渡,检查每步求精的一致性,尽可能早的找出程序的错误,从而降低程序开发成本。缺点是目前还没有很好的自动化验证工具用于验证求精中的每一步。
英文摘要: Software Architecture has been a hot research field in Software Engineering. This kind of method focuses on the overall organization of software system. It studies the interrelationships between components in an abstract level, therefore understands and analyses the behaviors and properties of the whole system in an overall and integrated view. It is very useful to develop large complex software. A question that frequently arises for architectural design is "How can I implement a system from a high-level architectural design to the low-level architectural design and eventually the final executable program?" This Problem involves architectural refinement methods. It's very important to assure the correctness of each refinement step. And this is also sour purpose in this thesis. Instead of refining an architectural design by another different style design in whole, Stepwise refinement programming design method based on components refines an architectural design by replacing a component's static semantics by its dynamic semantics. Because XYZ/E can represent static and dynamic semantics in a uniform frame, the transition from the specification of the component to its corresponding architecture structure designed at that step can be formally validated. The correctness of refinement can be verified by the tool XYZ/VERI based on Hoare logic ruls and verifying methods of temporal logic. In the thesis we first describe how to formalize components, connectors and architecture styles using temporal logic programming language XZY/E. Then it presents the programming method based on components and stepwise refinements from static semantics of dynamic semantics. This method combined software architecture and XYZ system effectively. Briefly, the process of programming by this methods includes: write specifications for the components according software requirements, select the proper architecture style, build sub-components and connectors, configure corresponding preferences, then create XYZ/E program, check the consistency of this program and the specification of the component. In this way, it assures that every refinement step is safe and correct. Do the same to the following sub-components, until there's no static description but dynamic semantics. The advantage of this method is that it can find the errors in program earlier and therefore reduce the development cost. The drawback is that there are not any well-perform automatic tools for verifying the correctness of refinement yet.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6314
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW004430.pdf(1980KB)----限制开放-- 联系获取全文

Recommended Citation:
郑建丹. 基于组件的逐步求精程序设计方法[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2001-01-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-2017  中国科学院软件研究所 - Feedback
Powered by CSpace