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

基于接口自动机的嵌入式软件验证技术及支撑工具研究

作　者: 徐丙凤
导　师: 胡军
学　校: 南京航空航天大学
专　业: 计算机应用技术
关键词: 嵌入式软件设计 构件化设计 软件验证 接口自动机 UML 模型检验工具
分类号: TP368.1
类　型: 硕士论文
年　份: 2009年
下　载: 51次
引　用: 0次
阅　读: 论文下载
 

内容摘要


现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术。由于嵌入软件具有极高的可靠性、严格的实时性以及资源、能耗使用的受限性,使得保证系统设计满足给定的功能规约以及满足非功能方面的严格限制成为嵌入式计算领域中的重要研究课题。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,而在系统设计前期缺乏有效工具对系统设计的功能性质以及非功能性质进行分析与验证。本文以接口自动机及其扩展模型作为构件化嵌入式软件的设计模型,以UML顺序图描述基于场景的功能规约,对基于接口自动机及其扩展模型的多个模型检验抽象算法进行分析且设计相应的算法实现框架。进而在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Design)。该工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题;另外,对非实时资源使用相关性质以及与时间相关的能耗性质进行分析和验证。工具设计与实现的主要内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现,最后通过两个具体的应用实例,介绍了该模型验证工具在嵌入式软件系统设计阶段的应用。

全文目录


摘要  4-5
ABSTRACT  5-8
图表清单  8-10
注释表  10-11
第一章 绪论  11-15
  1.1 课题研究背景及意义  11-12
  1.2 当前研究现状及选题依据  12-13
  1.3 论文的研究内容  13-15
第二章 接口自动机及其扩展模型  15-22
  2.1 接口自动机的非形式化描述以及形式化定义  15-18
    2.1.1 接口自动机的非形式化描述  15-17
    2.1.2 接口自动机的形式化定义  17-18
  2.2 接口自动机的扩展模型  18-21
    2.2.1 实时接口自动机模型  18-19
    2.2.2 资源接口自动机模型  19-20
    2.2.3 能耗接口自动机模型  20-21
  2.3 本章小结  21-22
第三章 基于场景规约的验证问题及抽象算法框架  22-34
  3.1 UML 顺序图的形式化描述  22-25
    3.1.1 UML 顺序图的形式化定义  22-24
    3.1.2 带时间约束的UML 顺序图模型  24-25
  3.2 接口自动机网络模型与兼容可达图  25-28
    3.2.1 接口自动机网络模型  25-28
    3.2.2 兼容状态空间的可达图  28
  3.3 关键问题以及相关抽象算法框架  28-33
    3.3.1 非实时功能行为验证  28-30
    3.3.2 实时功能行为验证  30-31
    3.3.3 资源性质验证  31-32
    3.3.4 能耗性质验证  32-33
  3.4 本章小结  33-34
第四章 T-CBESD体系结构以及功能验证模块的设计与实现  34-47
  4.1 现有模型验证工具的分析  34-36
  4.2 T-CBESD开发及运行环境  36
  4.3 T-CBESD体系结构以及界面设计  36-40
    4.3.1 T-CBESD体系结构  36-38
    4.3.2 T-CBESD界面设计  38-40
  4.4 功能验证模块的设计与实现  40-46
    4.4.1 功能验证模块的设计  40-41
    4.4.2 功能验证模块输入输出接口的设计实现  41-42
    4.4.3 UML 顺序图模型的输入预处理  42-43
    4.4.4 基本接口自动机组合模型的建立  43-44
    4.4.5 非实时功能行为验证算法的实现  44-46
  4.5 本章小结  46-47
第五章 T-CBESD非功能性质验证模块的设计与实现  47-58
  5.1 非功能性质验证模块的设计  47-48
  5.2 实时验证模块的设计与实现  48-51
    5.2.1 实时验证模块输入输出接口设计  48-49
    5.2.2 带时间约束的UML 顺序图的输入预处理  49-50
    5.2.3 实时接口自动机组合模型的建立  50
    5.2.4 实时功能性质验证算法的实现  50-51
  5.3 资源验证模块的设计与实现  51-55
    5.3.1 资源验证模块输入接口设计  51-53
    5.3.2 资源接口自动机组合模型的建立  53
    5.3.3 资源验证算法的实现  53-55
  5.4 能耗验证模块的设计与实现  55-57
    5.4.1 能耗验证模块输入接口设计  55-56
    5.4.2 能耗接口自动机组合模型的建立  56
    5.4.3 能耗验证算法的实现  56-57
  5.5 本章小结  57-58
第六章 T-CBESD的测试以及应用  58-69
  6.1 测试  58-59
  6.2 实例应用  59-68
    6.2.1 火灾预警组合系统实例应用  59-64
    6.2.2 通信构件组合系统实例应用  64-68
  6.3 小结  68-69
第七章 总结和展望  69-71
  7.1 总结  69-70
  7.2 展望  70-71
参考文献  71-75
致谢  75-76
在学期间的研究成果及发表的学术论文  76

相似论文

  1. 中小企业进销存管理系统的研究与设计,TP311.52
  2. UML模型到XMI的映射方法研究,TP311.5
  3. 基于模型的Web测试技术研究与应用,TP311.53
  4. 基于形式化UML测试序列生成方法研究,TP311.53
  5. 面向Seam框架的PIM到PSM转换研究,TP311.52
  6. 基于UML的体育场馆管理系统的分析、设计与实现,TP311.52
  7. 排课管理系统的设计与实现,TP311.52
  8. 振道科技人力资源管理系统,TP311.52
  9. 基于PDM的金融机具行业项目管理系统的研究与开发,TP311.52
  10. 永康市计生管理系统的设计与实现,TP311.52
  11. 教育局OA系统设计与实现,TP311.52
  12. 高校教务管理系统与实现,TP311.52
  13. 一个基于UML的提案管理系统的设计与实现,TP311.52
  14. 工程项目管理系统的设计与实现方法研究,TP311.52
  15. 面向家庭的远程健康监护系统的设计与研究,TP311.52
  16. 交通运输服务的GPS机动车监控系统的设计与实现,TN967.1
  17. 宜春学院学生就业管理系统的设计与实现,TP311.52
  18. 中小型物流企业配送管理系统的设计与实现,TP311.52
  19. 高校人力资源信息管理系统的设计和实现,TP311.52
  20. 基于J2EE的医院科研管理系统的设计与实现,TP311.52
  21. 市级电视台媒体资产管理系统的设计与实现,TP311.52

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 微型计算机 > 各种微型计算机 > 微处理机
© 2012 www.xueweilunwen.com