航天器中通过软件实现的功能越来越复杂,软件的可信性保障至关重要。中断数据访问冲突是当前影响航天嵌入式软件的关键可信问题之一,这个问题指的是,主程序和中断或者不同优先级中断同时对同一个共享数据进行访问导致数据一致性被破坏。中断数据访问冲突是一种典型的并发缺陷,非常难以测试发现。在航天软件研制过程中,目前主要依靠静态分析工具辅助人工审查进行检测,静态分析工具首先进行共享数据分析,在此基础上进行冲突检测,筛选出潜在的缺陷,最终经人工审查确认。但已有工具存在检测结果遗漏和误报高的问题,遗漏到航天器在轨运行等后续阶段的缺陷对任务成败产生影响,较高的误报增加了人工审查的成本。因此,需要进一步开展精确的中断数据访问冲突检测方法的研究和工具的研制,以减少现有工具的漏报和误报。中断数据访问冲突的检测包括共享数据分析和冲突检测两步,误报和漏报可能发生在任一步。本文针对上述两步存在的不足开展了研究:（1）针对已有共享数据分析方法难以识别I/O地址共享访问导致漏报和分析粒度难以精确到数组元素导致误报的问题,提出了基于抽象解释的中断共享数据分析方法。该方法通过一个通用的共享数据访问模型刻画各种粒度的共享数据访问情况,在此基础上对每个并发流入口进行基于抽象解释的数值分析,产生表示共享数据访问所需的数值不变式,最后对不同并发流下访问的数据进行共享分析得到共享访问点。（2）针对现有的中断原子性违反检测方法难以同时保证高精度和可扩展性的不足,提出了基于依赖图的原子性违反检测方法。该方法在中断共享数据分析得到的共享数据访问点集合上进行访问序模式匹配,筛选出潜在的原子性违反序列,再基于程序依赖图构建包含路径条件的中断摘要,通过约束求解来裁剪那些并发路径不可行的原子性违反序列,在实现精确检测的同时保证了可扩展性。在上述研究的基础上,设计并实现了中断共享数据分析工具Spec Checker-ISA和原子性违反检测工具int Atom,并选取真实的航天嵌入式软件和开源基准测试集对工具的有效性进行了评估。在4个真实航天嵌入式软件上对中断共享数据分析工具Spec Checker-ISA的实验结果表明,Spec Checker-ISA比现有工具多检测出1111个共享访问点,没有漏报,避免了61个误报,为中断数据访问冲突检测提供一个无漏报、低误报率的共享数据访问集合。对于原子性违反检测工具int Atom,在基准测试集上的实验结果表明,与最新研究结果相比误报率降低了72%,分析速度提高了3倍;在4个真实航天嵌入式软件上的实验结果表明,int Atom的平均误报率仅为19.4%,并能够在短时间内完成对数千行真实航天嵌入式软件的原子性违反检测,大大提升了现有工具的检测能力。