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

面向网构软件资源自适应的可信性研究

作　者: 夏琦
导　师: 王忠群
学　校: 安徽工程大学
专　业: 计算机应用技术
关键词: 网构软件 随机性资源 时限资源 接口自动机 模型检测
分类号: TP311.52
类　型: 硕士论文
年　份: 2013年
下　载: 7次
引　用: 0次
阅　读: 论文下载
 

内容摘要


计算平台正逐步从集中、静态和封闭向开放、动态、多变的因特网平台转变。因此,这种转变决定了未来的软件系统需要能够在Internet环境下具备开放的结构,拥有动态协同、在线演化、环境感知和自主适应的能力。Internet环境的开放性、动态性导致其提供给构件组合系统的资源具有不确定性、随机性,从而影响到构件组合系统的行为变化。如何对因环境资源的变化所导致的构件组合系统的行为变化进行有效分析和验证以提高网构软件系统的可信度给我们提出了挑战。网构软件的复杂性决定了资源自适应的可信性研究应从宏观层面入手。在网构软件的SA (Softwere Architecture)层次上,通过对构件随机性资源满足性以及资源满足是否具有时间约束的分析与验证来保证网构软件系统自适应的可信性。本文主要工作包含以下几个方面：1.针对网络环境的不确定性、随机性,通过对接口自动机进行随机性资源语义的扩展,称之为随机性资源接口自动机。研究随机性资源接口自动机网络,应用它来描述构件组合系统的行为,对系统的行为是否满足随机性的资源约束进行了验证,研究基于随机性资源接口自动机网络的可达图,并给出基于可达图的检测随机性资源的可满足性、最小资源需求量算法。2.针对构件组合系统是否满足时间约束的问题,通过对资源接口自动机进行时间约束方面的扩展,称之为时限资源接口自动机。使用时限资源接口自动机来建模构件组合行为,以及时限资源接口自动机网络来描述构件组合系统时限行为,研究基于时限资源接口自动机网络的可达图,并给出了基于可达图的检测构件满足资源是否具有时限约束的算法。3.通过使用上述模型对实例网上书店系统建模,说明模型的实际意义。4.最后,通过研究,将上述接口自动机模型转换为模型检测系统语言Promela,使用模型检测工具Spin对模型的正确性进行了验证。

全文目录


摘要  5-7
ABSTRACT  7-10
目录  10-12
第1章 绪论  12-17
  1.1 研究背景及意义  12-13
  1.2 相关研究现状  13-14
  1.3 论文主要工作  14-15
  1.4 论文组织结构  15-16
  1.5 本章小结  16-17
第2章 网构软件基本理论  17-21
  2.1 网构软件的提出  17-18
  2.2 网构软件的基本特征  18-19
  2.3 网构软件的发展  19-20
  2.4 本章小结  20-21
第3章 接口自动机理论  21-24
  3.1 接口自动机简介  21
  3.2 接口自动机的形式化定义  21-22
  3.3 接口自动机网络的形式化定义  22-23
  3.4 本章小结  23-24
第4章 构件的随机性资源满足性验证  24-34
  4.1 随机性资源接口自动机  24-28
    4.1.1 随机性资源接口自动机的非形式描述  24-25
    4.1.2 随机性资源接口自动机的形式化描述  25-26
    4.1.3 随机性资源接口自动机网络的形式化描述  26-28
  4.2 随机性资源满足的验证  28-32
    4.2.1 验证方法  28-29
    4.2.2 相关算法  29-32
      4.2.2.1 检查组合系统是否满足随机性资源约束算法  29-31
      4.2.2.2 组合系统运行资源最小量算法  31-32
  4.3 实例研究  32-33
  4.4 本章小结  33-34
第5章 构件的时限资源满足性验证  34-41
  5.1 时限资源接口自动机  34-36
    5.1.1 时限资源接口自动机的非形式描述  34-35
    5.1.2 时限资源接口自动机的形式化描述  35-36
    5.1.3 时限资源接口自动机网络的形式化描述  36
  5.2 资源满足是否具有时限性验证  36-39
    5.2.1 验证方法  37-38
    5.2.2 相关算法  38-39
  5.3 实例研究  39-40
  5.4 本章小结  40-41
第6章 基于Spin的系统模型验证  41-52
  6.1 模型检测工具Spin  41-42
    6.1.1 SPIN的历史背景  41
    6.1.2 SPIN的特征  41-42
  6.2 基于Spin的网构软件模型验证  42-51
    6.2.1 随机性资源接口自动机模型的验证  43-46
    6.2.2 时限资源接口自动机模型的验证  46-51
  6.3 本章小结  51-52
第7章 总结与展望  52-53
参考文献  53-56
攻读学位期间发表的学术论文目录  56-57
致谢  57

相似论文

  1. 面向服务实体的网构软件演化模型的研究,TP311.5
  2. 田野成像光谱仪中小麦叶绿素含量模型研究,S512.1
  3. 基于BMC的Web服务失配检测方法研究,TP311.52
  4. 基于谓词抽象与精化技术的Web服务验证研究,TP311.52
  5. 基于模型重建的软件测试及软件可靠性计算,TP311.53
  6. 基于SPIN模型检测的电子商务协议分析与验证,TP311.52
  7. 基于四方的安全电子商务支付协议研究,TP393.08
  8. 基于接口自动机的服务组合验证研究,TP393.09
  9. 安全协议自动化分析系统的设计与实现,TP393.08
  10. Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
  11. 基于UPPAAL的电子商务协议安全性分析,TP393.08
  12. 基于模型检测方法的可信软件验证技术研究,TP311.52
  13. 网构软件模型转换技术应用研究,TP311.52
  14. 基于接口自动机的嵌入式软件验证技术及支撑工具研究,TP368.1
  15. 面向环境演算系统的模型检测算法的研究,TP274
  16. 网络安全协议的模型检测分析及验证系统,TP393.08
  17. 基于约束系统模型的缓冲区溢出漏洞检测系统,TP393.08
  18. 基于程序语义的静态恶意代码检测系统的研究与实现,TP393.08
  19. 可重配置硬件系统调度算法的模拟与分析,TN791
  20. 基于L~*学习算法和假定—保证规则的组合验证,TP311.52
  21. 网构软件模型研究,TP311.5

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 软件工程 > 软件开发
© 2012 www.xueweilunwen.com