学位论文 > 优秀研究生学位论文题录展示

基于XYZ/SE的C/S体系结构风格研究

作　者: 刘曼霞
导　师: 张锦; 刘曙元
学　校: 湖南大学
专　业: 软件工程
关键词: 形式化方法 XYZ系统结构化XYZ/SE 体系结构风格
分类号:
类　型: 硕士论文
年　份: 2013年
下　载: 7次
引　用: 0次
阅　读: 论文下载

内容摘要

XYZ/SE是中国学者唐稚松教授历经二十余年研究而提出的第一种时序逻辑语言，由于其独特性而具有重要理论价值和应用前景，但遗憾的是自提出以来并未得到更为广泛的研究和应用。本文基于XYZ/SE时序逻辑语言对软件体系结构风格进行了研究。首先，本文详细介绍了XYZ/SE的关键语法，并提出了应用XYZ/SE对软件体系结构进行描述的一般流程。同时，基于逐步求精思想，以财税库银系统TIPS为对象研究了XYZ/SE的应用过程。即：（1）先将TIPS分解为各个组件（客户端组件、连接件、服务器组件及服务器子组件）并基于XYZ/SE完成TIPS的整体描述；（2）再基于XYZ/SE分别完成对各组件的形式化描述，以确保较高抽象层次与低层次之间语义的一致性。研究结果表明，XYZ/SE具备对不同抽象层次进行规范描述的能力，能实现从抽象（静态语义）到具体（动态语义）的平滑过渡。其次，研究了基于XYZ/SE的部分正确性验证规则的软件部分正确性验证问题。基于XYZ/SE对软件的形式化描述结果，提出了对应的软件部分正确性验证一般流程。然后以同一研究对象TIPS，在统一的XYZ/SE逻辑框架下，对XYZ/SE的形式化描述结果按照XYZ/SE的部分正确性验证规则逐步进行转换，直到得出部分正确性验证式子，从而直观地从静态上判断程序的部分正确性。研究表明，XYZ/SE可以在统一框架下表达出Hoare逻辑推演规则，实现了形式化描述与部分正确性验证的统一，简化了程序部分正确性的验证。

全文目录

摘要  5-6
Abstract  6-9
插图索引  9-10
第1章绪论  10-18
  1.1 研究背景与意义  10-13
  1.2 国外内研究现状  13-16
  1.3 本文研究内容  16-17
  1.4 本文章节安排  17-18
第2章 XYZ 系统  18-24
  2.1 XYZ系统  18-19
    2.1.1 产生背景  18-19
    2.1.2 系统概述  19
  2.2 时序逻辑语言XYZ/E  19-22
    2.2.1 状态转换与单元  20
    2.2.2 通信  20-21
    2.2.3 控制结构  21-22
  2.3 结构化XYZ/E（XYZ/SE）  22-23
  2.4 小结  23-24
第3章基于 XYZ/SE 的体系风格描述  24-38
  3.1 软件体系结构风格  24-26
    3.1.1 体系风格形式化  24-26
      3.1.1.1 组件  24-26
      3.1.1.2 连接件  26
    3.1.2 C/S体系结构风格形式化  26
  3.2 求精技术  26-28
    3.2.1 求精技术概述  26-28
    3.2.2 软件体系结构求精  28
  3.3 财税库银系统的软件风格  28-32
    3.3.1 财税库银系统  28-30
    3.3.2 财税库银系统业务处理流程  30
    3.3.3 财税库银系统的C/S体系风格架构  30-32
  3.4 基于XYZ/SE的TIPS风格描述  32-37
    3.4.1 整体描述  32-33
    3.4.2 组件描述  33-37
      3.4.2.1 BRClient组件描述  33-34
      3.4.2.2 连接件MP描述  34-35
      3.4.2.3 GNServer组件描述  35-36
      3.4.2.4 Computation组件描述  36-37
  3.5 小结  37-38
第4章基于 XYZ/SE 的部分正确性验证  38-50
  4.1 部分正确性验证  38-39
  4.2 基于XYZ/SE的部分正确性验证思想  39-41
    4.2.1 验证规则  39-41
    4.2.2 验证步骤  41
  4.3 基于XYZ/SE的TIPS风格验证  41-49
    4.3.1 整体验证  41-43
    4.3.2 组件验证  43-49
      4.3.2.1 BRClient组件验证  43-44
      4.3.2.2 MP连接件验证  44-46
      4.3.2.3 GNServer组件验证  46-47
      4.3.2.4 Computation组件验证  47-49
  4.4 小结  49-50
结论与展望  50-52
参考文献  52-57
致谢  57-58
附录 A 攻读硕士学位期间发表的论文  58-59
附录 B 攻读学位期间所参与的主要项目  59

相似论文

基于PVS的自稳定算法形式化分析,TP338.8
PDF文件处理系统,TP311.52
软件体系结构复用的研究,TP311.52
电子商务协议的形式化分析,F713.36
基于组件的逐步求精程序设计方法,TP311.52
基于UML的软件体系结构六视图描述研究,TP311.52
一种基于Agent的软件体系结构风格研究,TP311.52
软件体系结构建模研究与应用,TP311.52
基于BDI模型和ARCHON模型的MAS动态软件体系结构风格研究,TP311.52
智能系统集成环境中ADL的应用研究,TP311.52
基于MAS技术遗留系统包装器体系结构风格的研究,TP311.52
串空间方法分析安全协议,TP393.04
自适应对象模型体系结构风格的应用研究,TP311.52
软件体系结构在光盘库系统设计中的研究及应用,TP311.52
安全协议模型检验技术研究与实现,TP393.08
基于串空间模型分析与验证密码安全协议,O157.4
基于反例搜索的启发式模型检测算法的研究,TP311.52
软件体系结构在电力遥视系统开发中的应用,TM769
基于企业业务框架的软件体系结构研究,TP311.5
软件自适应若干关键技术研究,TP311.52
软件体系结构形式描述研究,TP311.52