基于组件的逐步求精程序设计方法
文献类型:学位论文
作者 | 郑建丹 |
学位类别 | 博士 |
答辩日期 | 2001 |
授予单位 | 中国科学院软件研究所 |
授予地点 | 中国科学院软件研究所 |
关键词 | XYZ系统 时序逻辑语言 软件体系结构 逐步求精 形式化方法 |
学位专业 | 计算机软件与理论 |
中文摘要 | 软件体系结构是近年来软件工程界的热门研究领域之一。在软件体系结构设计过程中,经常要碰到的问题是如何从抽象的高层体系结构逐步过渡到底层的体系结构直到最后的实现。这个过渡过程要保证每层过渡的正确性,否则最后得到的可执行程序可能不是最初所想要的目标程序,因此如何对体系结构求精显得尤其重要。这也是本文要致力解决的问题。基于组件的由静态语义向动态语义逐步过渡的程序设计方法从体系结构的基本元素-组件入手,用XYZ/E形式化体系结构,每次的求精都是对组件的求精,而不是整个体系结构,组件的求精就是用组件的动态语义代替组件的静态语义,由于XYZ/E具有可以在统一的框架下描述静态语义和动态语义的特点,从而使系统能够从最初的体系结构设计平滑到最后的可执行程序。求精一致性的验证可以借助于基于Hoare逻辑规则的验证工具XYZ/VERI以及XYZ/E作为时序逻辑语言所具有的对一些程序性质的证明方法。本文首先用时序逻辑语言XYZ/E形式化描述体系结构中的基本组件和连接件以及体系结构风格,说明如何用XYZ/E描述软件体系结构然后在此基础上提出基于组件的由静态语义向动态语义逐步过渡的程序设计方法,将软件体系结构XYZ系统有机的结合起来。这种方法的优点是在统一的框架下描述不同抽象程度的体系结构,使体系结构的第一步求精能够平滑的过渡,检查每步求精的一致性,尽可能早的找出程序的错误,从而降低程序开发成本。缺点是目前还没有很好的自动化验证工具用于验证求精中的每一步。 |
语种 | 中文 |
公开日期 | 2011-03-17 |
页码 | 50 |
源URL | [http://ir.iscas.ac.cn/handle/311060/6314] ![]() |
专题 | 软件研究所_中科院软件所_中科院软件所 |
推荐引用方式 GB/T 7714 | 郑建丹. 基于组件的逐步求精程序设计方法[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2001. |
入库方式: OAI收割
来源:软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。