信息物理系统(Cyber Physical Systems,简称CPS)作为当今世界信息技术制高点,已广泛应用于电力系统、医疗仪器设备、航空航天等安全攸关领域。由于CPS是一种综合了计算进程与物理环境的新型网络化嵌入式系统,故包含种类和数目众多的嵌入式软件,且各软件通过网络交互,因此如何保障这些异构软件及其交互过程可信性已成为CPS研究热点之一。软件可信性保障涉及软件开发过程的众多方面,本文拟在软件设计阶段,研究适用于CPS软件的形式化建模方法、验证方法以及分析技术,具体解决以下四方面CPS软件可信性保障问题:针对CPS软件功能与实时性验证问题,提出了基于时间状态迁移矩阵(Time State Transition Matrix,简称TSTM)软件形式化建模方法。TSTM在保持原状态迁移矩阵形式语义基础上,引入时钟函数与时间约束,使其适用于实时CPS软件行为刻画。在此基础上,提出了基于时间计算树逻辑(Time Computation Tree Logic,简称TCTL)的TSTM模型检测方法,为有效缓解状态空间爆炸,模型检测方法采用限界模型检测(Bounded Model Checking,简称BMC)技术。实验表明本文所提验证方法具有较好的求解效率,实现了在软件设计层面逻辑功能与时间性能的一体化建模与验证。针对CPS软件能耗预测与分析问题,提出了基于能耗时间状态迁移矩阵(Energy Consumption Time State Transition Matrix,简称 ETSTM)的绿色软件形式化建模方法。ETSTM在TSTM基础上,引入基于软件结构特征量的能耗预测函数,并给出了基于BP神经网络(Back-Propagation neural network)的能耗预测函数拟合方法。在此基础上,提出了基于显示路径搜索和限界模型检测的CPS软件能耗多尺度分析算法。最后,通过实验验证了本文所提方法的有效性,实现了在软件设计层面对CPS软件能耗的预评价,避免在软件开发后期因能耗等绿色指标不满足设计约束而重新设计开发。针对CPS软件动态性能评价问题,提出了基于扩展的确定与随机Petri网(Extended Deterministic and Stochastic Petri Nets,简称 EDSPN)的 CPS 软件行为模型。通过为确定与随机Petri网模型增加非确定时间语义,使其能够有效表示由中断嵌套带来的低优先级程序执行时间不确定问题,进而实现对中断驱动下的CPS软件行为有效建模。此外,针对EDSPN模型分析,提出了一种基于马尔科夫再生理论(Markov Regenerative Theory,简称MRT)的模型求解方法,给出了变迁抢占策略、再生点选取方法、非确定时间变迁上限执行时间计算方法以及稳态概率求解方法。最后,通过实验分析了 CPS软件在多优先级中断抢占执行下的服务性能,讨论了中断触发频率、中断服务时间、中断优先级数量等因素对CPS软件性能的影响。针对CPS软件非确定行为分析问题,提出了与EDSPN压缩可达图同构的标记马尔科夫再生过程(Labeled Markov Regenerative Processes,简称LMRGP)的形式化定义。以该模型为基础,提出了基于BMC策略的连续随机逻辑(Continuous Stochastic Logic,简称CSL)概率模型检测方法。最后,通过分析具有多级中断的CPS软件模型,定量分析了 CPS软件的非确定行为,并在实验中比较了 BMC方法与非BMC方法的求解能力,验证本文所提方法的有效性。