陈 睿，杨孟飞

(1.北京控制工程研究所，北京 100190； 2.北京轩宇信息技术有限公司，北京 100190；3.中国空间技术研究院，北京 100190)



基于编码规则的中断数据访问冲突检测方法*

陈 睿1,2，杨孟飞3

(1.北京控制工程研究所，北京 100190； 2.北京轩宇信息技术有限公司，北京 100190；3.中国空间技术研究院，北京 100190)

针对“重复加锁解锁”和“volatile修饰符误用”两种数据访问冲突缺陷模式，提出基于编码规则的检测方法.首先，对缺陷模式的故障机理进行分析，提炼出3条编码规则用以在开发阶段避免缺陷发生，并基于一个静态代码检查工具SpaceCCH进行了规则检测方法研究和实现.在实际星上软件上的实验结果表明，扩展的SpaceCCH能够高效、低误报、低漏报地发现规则违反，从而有效避免这两种的数据访问冲突问题.本文的贡献在于将一类复杂缺陷的检测转换为相应的编码规则及其检测. 关键词： 数据访问冲突；编码规则；静态分析；航天嵌入式软件

0 引 言

数据访问冲突问题是当前航天型号软件开发中最难解决的问题之一[1].这类问题发生在中断驱动型程序或多任务程序中，当两个不同的中断(或任务)对同一个共享数据进行同时的读写访问，且至少存在一次写操作时.由于两次访问的时序不可确定，程序会产生异常行为，如关键数据被非预期地修改，严重时甚至导致系统或软件失效.然而，数据访问冲突问题发生概率小、难以复现，往往在特殊的外部条件和中断(或任务)交迭情况下才会出现，难以通过传……