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

关键词:嵌入式软件设计,接口自动机,UML 交互概观图, 即时验证算法,形式化验证
i
基于即时验证的嵌入式软件验证技术研究
ABSTRACT
Model-based techniques for system designs and analysis can effectively satisfy high reliability
requirements of modern embedded software system. Embedded software has the requirements of high
reliability, real-time constraints, resource restrictions, and domain-specific adaptation with respect to
general systems. Therefore, how to guarantee system designs meet the given function specification
and the non-function restriction is ing one of the active research issues in puting
domain currently.
In puting domain, traditional methods mostly concern the implementation and
testing phrase, without effective tools supporting the analysis and verification of the system designs in
the design phrase. In this thesis, we do research on On-the-fly verification techniques for embedded
software designs. We use UML interactive overview diagram as the scenario-based specification and
the interface automata and its extension models to model embedded software systems. Then, we
develop several algorithms based on On-the-fly verification mechanism to attack the analysis and
verication problems of the functional and non-functional properties which are mostly concerned
during the dev