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

基于形式化方法的统一软件模型及其应用

作　者: 邢金亮
导　师: 李晓红
学　校: 天津大学
专　业: 计算机应用技术
关键词: 可信软件软件工程软件安全形式化方法
分类号: TP311.52
类　型: 硕士论文
年　份: 2010年
下　载: 58次
引　用: 0次
阅　读: 论文下载

内容摘要

随着计算机应用的不断发展,在信息社会中发挥着至关重要的作用。但是软件的生产现状不能令人满意,软件安全事故、软件质量问题、软件扩展问题已经带来了巨大的损失。国内外专家及行业巨头已经将软件的可信性作为软件的一个重要属性,然而,目前多数研究主要还是针对安全性。本文将软件可信性做一个多维的评估指标,通过软件工程方法论的角度,针对软件的功能性、可靠性、安全性、可维护性、可扩展性等性质进行了研究,主要工作包括:1)提出了基于形式化语言Z规格和UML视图的统一软件模型,基于该模型,构建了软件可信工程方法,该方法将形式化方法融入传统软件工程,继承了形式化模型可验证的优点,并一定程度降低了形式化模型在大型项目中较高的复杂度、和传统软件工程大量的人为不确定因素。2)基于课题组软件安全缺陷知识库,实现了统一软件模型在设计阶段的软件安全缺陷形式化检测,从而在缺陷引入的最早阶段快速发现并给出具体缓和方案,避免了设计阶段的软件安全缺陷在软件生命周期后期非常高昂的缓和成本、降低了软件安全性保障对安全专家个人经验和知识的依赖。3)设计了软件可信工程支持平台,从工具角度提高了软件可信工程的可实施性,并引入了结合统一软件模型的项目管理机制降低了工程管理所引入的开发不确定性。本文搭建了一个结合了形式化方法的软件工程理论体系,实现了软件设计的一致性、有效性、安全性验证,集成了课题组其他工作如模型驱动的单元测试、可信性评估等,同时,为将来的研究工作提供了理论基础。

全文目录

摘要  3-4
ABSTRACT  4-6
第一章绪论  6-14
  1.1 研究背景及相关工作  6-11
  1.2 研究动机和意义  11-12
  1.3 主要工作和贡献  12-13
  1.4 论文组织结构  13-14
第二章软件可信工程  14-19
  2.1 软件可信工程  14-16
  2.2 软件可信工程支持平台  16-17
  2.3 软件可信工程最佳实践方案  17-19
第三章统一软件模型  19-33
  3.1 统一软件模型的构成  19-22
  3.2 统一软件模型的一致性、有效性验证  22-26
    3.2.1 定理证明验证方法综述  22-24
    3.2.2 统一软件模型的一致性验证  24
    3.2.3 统一软件模型的有效性验证  24-26
  3.3 统一软件模型的安全性验证  26-33
    3.3.1 软件缺陷的Z规格形式化描述  27-28
    3.3.2 统一软件模型Z规格基础框架  28-30
    3.3.3 通过Z/EVES实现安全性验证  30-33
第四章软件可信工程支持平台的实现  33-44
  4.1 统一软件模型设计平台  33-35
  4.2 统一软件模型安全性验证模块  35-39
  4.3 功能单元开发平台  39-40
  4.4 应用实例  40-44
第五章总结与展望  44-45
参考文献  45-49
发表论文和参加科研情况说明  49-50
致谢  50

基于形式化方法的统一软件模型及其应用

内容摘要

全文目录

相似论文