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