目前嵌入式软件应用日益广泛,软件规模越来越大,动辄上千万行C代码;大量采用定时器,逻辑结构复杂;存在中断多级嵌套以及CPU+GPU+FPGA异构的特点,导致软件开发和测试极为困难,这类软件的可信问题是安全关键行业面临的主要问题。从可信软件的角度来看,嵌入式软件可信至少应该包括功能可信和性能可信。所谓功能可信是指软件完成预期的功能,即软件执行的正确性;性能可信是指软件在规定的时限之内完成预期的任务,否则即使执行正确也没有意义。目前可信软件研究更多集中在功能可信研究,在软件测试、软件形式化建模、模型仿真与验证等方面进行研究并取得一些成果。但是,嵌入式系统设计不但要解决功能可信问题,还需要解决性能可信问题。性能可信主要包括:（1）如何验证软件的正确性和时间性能;（2）如何对中断驱动程序进行时间分析和调度;（3）如何确定任务处理顺序以保证多核嵌入式系统实时性;（4）如何降低嵌入式系统能耗等问题。针对上述问题,本文围绕嵌入式系统的性能可信问题,从可信验证、中断调度、任务调度和能耗优化等4个方面展开探索和研究,具体内容如下:（1）嵌入式软件需求建模与验证理论方法研究针对嵌入式软件需求可信验证问题,提出基于扩充的状态迁移矩阵（Extended State Transition Matrix,简称ESTM）的嵌入式系统需求形式化建模方法,该方法通过在状态迁移矩阵（State Transition Matrix,简称STM）中增加时钟映射函数结构,可以有效表示事务处理时间,使ESTM模型具有显示时间属性能力;以ESTM模型为基础,针对功能验证问题,采用基于有界模型检测（Bounded Model Checking,简称BMC）技术的时间命题时序逻辑（Timed Propositional Temporal Logic,简称TPTL）模型检测方法,验证系统的功能属性以保证软件执行的正确性;针对性能验证问题,设计一种基于插值的模型验证方法（Model Verification Method based on Interpolation,简称 MVMI）,根据事件处理函数和状态迁移过程,计算程序执行路径复杂度的符号性范围,为判定软件设计的时间性能是否能够满足要求提供重要依据,对系统潜在的性能问题进行预警。（2）中断驱动程序的形式化建模和调度研究在实时嵌入式软件设计中,时间可预测性是确保软件可靠性的一个至关重要的因素。所以,时间分析是一个十分重要并具有挑战性的问题。本研究从时序的角度出发提出中断驱动程序的形式化建模方法和中断线程调度算法。首先,采用中断扩充状态迁移矩阵（Interrupt Extended State Transition Matrix,简称IESTM）形式化方法对中断驱动程序进行建模,给出操作语义和程序语义的定义,使用该语义分析程序的时间特性,并提供安全机制保障主程序在截止期限之前执行完成。其次,针对中断线程调度提出IEDF调度算法,算法能够减少中断线程执行所需的等待时间并且有效降低截止期错失率,减少中断处理的时间消耗,保证系统的实时性能。（3）多核嵌入式实时系统优化调度模型在嵌入式实时系统中,任务的实时性不仅仅是要保证任务及时响应,更重要的是要保证任务按时完成,即在保证高优先级任务实时性的同时,也要尽量保证低优先级任务的实时性,从而保证整个系统的实时性。本研究提出多核嵌入式实时系统优化调度模型,该模型采用分散调度方式设置两级调度算法,第一级调度算法主要功能是为多核心分配任务,主要目的是减少核心上任务的总等待时间;第二级调度算法主要功能是对核心上的任务进行调度,主要目的是保证整个系统的实时性,设计一种插入延迟时间的调度算法。（4）嵌入式实时系统能耗感知动态调节模型嵌入式系统一般工作在能耗受限环境中,因此在满足CPU计算性能的前提下,必须考虑能耗因素。本研究提出嵌入式实时系统能耗感知调节模型,将任务调度与能耗管理相结合,既保证任务在截止期限之前执行完成,又尽量降低处理机能耗。从时序控制和能耗控制两个方面考虑,设计出动态能耗管理调度算法,充分探讨有多个抢占任务条件下,兼顾任务的截止期限和系统能耗调节,采用DVFS技术在满足截止期限的同时降低系统能耗。