嵌入式软件在关键领域的广泛应用使其对可信性的需求远远高于一般软件。由于嵌入式软件在体系架构、资源限制、应用环境等方面的特殊性,以及近年来复杂化、规模化与开放化的发展趋势,保障和评估嵌入式软件的可信性已成为国内外越来越关注的研究热点之一。在嵌入式软件开发早期对其可信性进行分析、验证与评估,能够减少潜在的软件缺陷,从而降低后期测试与维护的成本。本文立足于可信嵌入式软件的建模与验证问题,旨在建立基于模型驱动的嵌入式软件建模与验证集成框架;采用Z语言为该框架提供形式化语义,针对嵌入式软件可信属性开展建模、验证与评估技术的研究;设计并实现了相应的原型系统,在嵌入式软件实例上进行应用研究。论文研究工作的主要创新性成果如下:(1)根据嵌入式软件的可信需求,提出了一种嵌入式软件形式化模型Z-MARTE,包括Z-MARTE时间模型、结构模型与行为模型。与现有模型相比,Z-MARTE是一种静态结构与动态行为的综合模型,能够同时描述嵌入式软件功能结构、时序行为以及可信约束。在Z-MARTE模型中引入了可信构造型的概念,通过对可信构造型的声明与约束,能够描述包括数据约束与时间约束在内的各类可信约束,为嵌入式软件可信性的验证与评估提供形式化语义基础。(2)为了对Z-MARTE模型描述的可信约束进行自动验证,提出了一种基于模型检测技术的嵌入式软件可信验证方法。首先,给出了有限域上Z-MARTE行为模型的语义解释,为模型检测方法提供了行为语义基础;其次,扩展了CTL的语法与语义,定义了一种描述嵌入式软件可信性质的时序逻辑公式ZMTL;最后,设计了有限域Z-MARTE行为模型上的模型检测算法FZMCA,能够在有限域内对Z-MARTE模型中的实时性、安全性等可信性质进行自动验证。(3)为了对Z-MARTE模型进行进一步的评估与分析,提出了一种嵌入式软件风险评估方法RAMES。首先,对Z-MARTE结构模型进行精化与扩展,提出了一种嵌入式软件对象-消息-角色模型OMR;在此基础上提出了风险分析算法RAOMR,以OMR模型中的嵌入式软件对象为评估单位,以对象间的通信行为与软件安全约束为评估依据进行风险评估,并进行了算法复杂度分析与实例研究。RAMES方法遵循ISO 31000标准的风险管理过程,其评估结果能够指导嵌入式软件设计模型中安全资源的合理分配。(4)在上述研究成果的基础上,建立了一个嵌入式软件可信性建模与验证集成框架,设计并初步实现了一个原型系统。在Eclipse平台上初步实现了一个基于XSLT转换技术的模型转换工具ZMT,将半形式化建模环境Open Embe DD与形式化建模环境CZT进行了集成;在VC 6.0平台上,对Z-MARTE模型解析模块、Z-MARTE行为模型生成模块与FZMCA模型检测模块进行了研究与实现;最后,对原型系统的应用技术进行了研究。