基于抽象解释的多中断程序数据访问冲突检测方法

摘要

本发明公开一种基于抽象解释的多中断程序数据访问冲突检测方法，步骤为：1）将中断驱动型程序采用抽象解释框架进行描述，每个任务中其他任务对目标共享变量的修改及修改条件抽象为一条干扰信息，每个任务中所有干扰信息构成一个干扰信息集合，通过迭代计算输出稳定的干扰信息集合；2）收集所有任务的干扰信息集合构成一个全局干扰信息集合，通过迭代计算获得稳定的全局干扰信息集合；3）使用稳定的全局干扰信息集合对每个任务进行遍历，若全局干扰信息集合中存在同时满足目标共享变量修改条件的干扰信息，判定为存在数据访问冲突。本发明具有实现方法简单、复杂度低、准确性及可靠性高的优点且适用于航天嵌入式软件的检测。

主权项

一种基于抽象解释的多中断程序数据访问冲突检测方法，其特征在于，步骤为：（1）任务间影响的抽象：将每一个中断驱动型程序作为一个任务并采用抽象解释框架进行描述，将每个任务中其他任务对目标共享变量的每一次修改及每一次修改的修改条件抽象为一条干扰信息，每个任务中对目标共享变量的所有干扰信息构成一个干扰信息集合；对每个任务的干扰信息集合独立的进行迭代计算，直到所有的任务获得稳定的干扰信息集合；（2）获得稳态干扰：收集所有任务对应的稳定干扰信息集合构成一个全局干扰信息集合，通过迭代计算获得稳定的全局干扰信息集合；每次迭代时，输入全局干扰信息集合并将全局干扰信息集合遍历每个任务，每个任务经过迭代后得到一个任务间相互影响后的目标干扰信息集合，所有任务的目标干扰信息集合合并后作为下一次迭代的输入，直到全局干扰信息集合达到不动点；（3）访问冲突检测：使用稳定的全局干扰信息集合对每个任务进行遍历，待检测任务对目标共享变量进行访问时，若全局干扰信息集合中存在同时满足目标共享变量修改条件的干扰信息，判定为存在数据访问冲突；所述步骤（1）中对中断驱动型程序进行抽象解释的具体方法为：（1.1）对中断驱动型程序进行形式化描述，将主任务和中断驱动型程序统一作为整个系统的任务，每个任务抽象为程序语句以及任务所对应的优先级；（1.2）对中断驱动型程序进行语义解释，描述中断驱动型程序在执行时的形态，由中断驱动型程序的具体执行状态得到状态迁移函数。