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

1、基于接口自动机的嵌入式软件验证技术及支撑工具研究    英文题名 Research on Interface Automata Based Embedded Software Verification Techniques and Supporting Tools  关键词 嵌入式软件设计; 构件化设计; 软件验证; 接口自动机; UML; 模型检验工具; 英文关键词 Embedded software design; Component-based design; Software verification; Interface Automa

2、ta; UML; Model checking tool; 中文摘要 现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术。由于嵌入软件具有极高的可靠性、严格的实时性以及资源、能耗使用的受限性,使得保证系统设计满足给定的功能规约以及满足非功能方面的严格限制成为嵌入式计算领域中的重要研究课题。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,而在系统设计前期缺乏有效工具对系统设计的功能性质以及非功能性质进行分析与验证。 本文以接口自动机及其扩展模型作为构件化嵌入式软件的设计模型,以UML顺序图描述基于场景的功能规约,对基于接口自动机及其扩展模型的多个模型检验抽象算法进行分析且设

3、计相应的算法实现框架。进而在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Design)。该工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题;另外,对非实时资源使用相关性质以及与时间相. 英文摘要 High reliability requirements of modern embedded s

4、oftware system need effective model-based techniques for system designs 摘要 4-5 ABSTRACT 5 图表清单 8-10 注释表 10-11 第一章 绪论 11-15     1.1 课题研究背景及意义 11-12     1.2 当前研究现状及选题依据 12-13     1.3 论文的研究内容 13-15 第二章 接口自动机及其扩展模型 15-22     2.1 接口自动机的非形式化描述以及形

5、式化定义 15-18         2.1.1 接口自动机的非形式化描述 15-17         2.1.2 接口自动机的形式化定义 17-18     2.2 接口自动机的扩展模型 18-21         2.2.1 实时接口自动机模型 18-19         2.2.2

6、资源接口自动机模型 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

7、.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 非实时功能行为

8、验证 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 现有模型验证工具的分

9、析 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     

10、0;   4.4.1 功能验证模块的设计 40-41         4.4.2 功能验证模块输入输出接口的设计实现 41-42         4.4.3 UML 顺序图模型的输入预处理 42-43         4.4.4 基本接口自动机组合模型的建立 43-44         4.4.5

11、非实时功能行为验证算法的实现 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

12、 顺序图的输入预处理 49-50         5.2.3 实时接口自动机组合模型的建立 50         5.2.4 实时功能性质验证算法的实现 50-51     5.3 资源验证模块的设计与实现 51-55         5.3.1 资源验证模块输入接口设计 51-53       &

13、#160; 5.3.2 资源接口自动机组合模型的建立 53         5.3.3 资源验证算法的实现 53-55     5.4 能耗验证模块的设计与实现 55-57         5.4.1 能耗验证模块输入接口设计 55-56         5.4.2 能耗接口自动机组合模型的建立 56     

14、0;   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 &#

15、160;   6.3 小结 68-69 第七章 总结和展望 69-71     7.1 总结 69-70     7.2 展望 70-71 参考文献 71-75     4.2 T-CBESD开发及运行环境 36     4.3 T-CBESD体系结构以及界面设计 36-40         4.3.1 T-CBESD体系结构 36-38     

16、    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  

17、       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   

18、60;     5.2.1 实时验证模块输入输出接口设计 48-49         5.2.2 带时间约束的UML 顺序图的输入预处理 49-50         5.2.3 实时接口自动机组合模型的建立 50         5.2.4 实时功能性质验证算法的实现 50-51     5.3 资源验证模块的设计与实

19、现 51-55         5.3.1 资源验证模块输入接口设计 51-53         5.3.2 资源接口自动机组合模型的建立 53         5.3.3 资源验证算法的实现 53-55     5.4 能耗验证模块的设计与实现 55-57         5.4.1 能

20、耗验证模块输入接口设计 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     &

21、#160;   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     4.2 T-CBESD开发及运行环境 36     4.3 T-

22、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       &

23、#160; 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非功能性质验证模

24、块的设计与实现 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