基于即时验证的嵌入式软件验证技术研究

发布时间：2020-08-26 00:58

【摘要】：基于模型的设计与分析技术是现代复杂嵌入式软件系统高可靠性的重要保障手段。与一般的软件系统相比,嵌入式软件具有极高的可靠性、严格的实时性以及可使用资源的受限性、满足特定领域等要求。如何保证系统设计满足给定的功能规约,以及满足实时、资源、能耗等非功能方面的严格限制,提高软件的可靠性已成为嵌入式计算领域中的重要研究课题。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,而在软件设计与分析的前期阶段还缺乏有效的方法和工具来支持对系统设计的分析与验证。本文对基于即时验证的嵌入式软件验证理论和技术进行深入研究,采用UML交互概观图模型描述基于场景的系统规约,以接口自动机及其扩展模型作为嵌入式软件系统设计模型,设计相应的即时验证算法(On-the-fly verification algorithm),对嵌入式软件设计阶段有关系统动态行为的功能及非功能属性进行形式化分析与验证。根据所设计的即时验证算法,在Eclipse平台上对一个构件化嵌入式软件设计模型的原型验证工具T-CBESD进行扩展设计与实现,以提高原型工具的验证效率与实用性。主要工作包括:扩展工具的输入接口,改进工具的核心算法,实例研究,证明即时验证算法的高效性和准确性。扩展后的工具为现代复杂嵌入式软件系统设计提供了有效的基于模型的分析与验证工具。
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2010
【分类号】：TP368.1
【图文】：

界面图,自动机模型,能耗,工具

南京航空航天大学硕士学位论文接口。但工业界已有一些比较成熟的形式化图形工具，提供了绘制基AP[44]。JFLAP为我们提供了方便易用的有限自动机建模接口，并提供一些文本和标签的功能。为此，对于接口自动机的图形化建模而言，P。其原因有二：首先，JFLAP是基于Java的开源系统，很容易集成到P提供了良好的建立有限自动机的建模机制，虽然无法直接通过JFLA但是可以通过在JFLAP的自动机模型中添加合适的语法结构来表达接义信息，并通过进一步的处理来获得满足T-CBESD输入格式要求的模建立能耗接口自动机模型界面。

顺序图,概观,图模型,图书馆

图 3.1 图书馆借书系统 UML 交互概观图模型动图和顺序图的结合体，直观地表达一组相关顺序图图和顺序图的形式化说明的基础上给出的。以下给出观图、实时交互概观图的形式化定义：语义如下[46]：：一个活动图是一个六元组，D=(A，T，F，G，ai，…，am｝是一个有穷的活动状态集；…，tn｝是一个有限完成跃迁集；∪龴T×A）是流关系；的条件表达式；活动状态，af∈A 是终止活动状态； t 满足龴ai，t）∈F；T，（tj，ai） F 且（af，tj） F。语义如下[9]：

模型图,工具,活动图,概观

南京航空航天大学硕士学位论文十分必要的。对于交互概观图的建模而言，目前还不存在提供直接绘制化建模工具。但是我们发现工具 Topcased[47]提供了一种间接绘制的方e 插件，支持多种 UML 模型图的绘制，提供了绘制活动图并可以用相关功能。即：可以在 Topcased 中，先绘制活动图对系统运行流程进行建对活动图中的一些关键节点进行细化，用于描述系统运行时的某个具体概观图描述系统规约的功能。因此，我们选择 Topcased 作为 UML 交互模接口。图 3.2 给出了 Topcased 工具绘制规约模型的界面。

【参考文献】