1.一种结合符号执行和路径模型检验的MPI程序验证方法，其特征在于实施步骤包括：1)输入目标MPI程序、给定性质 以及符号变量集合Sym；2)初始化符号执行待探索状态列表Worklist为目标MPI程序的全局初始状态init；3)按照指定的路径空间搜索策略从符号执行待探索状态列表Worklist中选取一个尚未处理的待探索状态S c ；4)按照轮询调度策略，选取待探索状态S c 下的活跃进程i，其状态包括该进程的变量取值映射关系M i 、下一条待执行语句Stat i 、进程路径条件PC i 和进程运行状态F；5)基于待探索状态S c 对活跃进程i的待执行语句Stat i 进行符号执行，并更新进程i的状态s i ；判断S c 中所有进程是否已经终止，是则执行步骤6)；否则执行步骤3)；6)到达此步骤表明符号执行已经探索完一条正常终止的路径，记为p；根据路径p所产生的通信行为信息生成用于精确模拟路径p的等价通信行为的CSP模型Γ，此处路径p的等价通信行为是改变p中通信操作的交叠执行情况和消息匹配情况所产生的通信行为；7)调用CSP模型检验工具来验证模型Γ是否满足性质 如果满足则从Worklist中裁剪掉符号执行探索路径p时为通信操作的不同交叠执行情况和不同匹配情况所创建的待探索状态，并继续执行步骤8)；如不满足则产生违背性质 的反例，生成相应测试用例并结束退出；8)判断符号执行待探索状态列表Worklist是否非空，非空则跳转执行步骤3)；否则，终止并退出；步骤6)中生成用于精确模拟路径p的等价通信行为的CSP模型Γ的具体步骤包括：6.1)确定待建模的执行路径p和产生该路径的MPI进程个数n；6.2)初始化存放CSP进程的集合PS为空集；初始变量i为0；6.3)以第i号MPI进程作为当前建模进程，确定进程i在探索路径p时所流出的MPI通信操作序列Seq i 和Seq i 的长度m；初始变量j为m-1，初始CSP进程P i 为Skip，执行步骤6.4)为进程i生成对应的CSP进程P i ，并将P i 加入到集合PS中；判断i是否等于n，是则跳转执行步骤6.5)，否则将i的值增加1继续执行步骤6.3)；6.4)针对通信操作序列Seq i 中的通信操作op j 的类型为其生成相应的CSP事件；若op j 为阻塞通信操作，将生成的事件顺序组合在P i 之前来更新P i ，否则将该事件与P i 进行并行组合来更新P i ；判定j是否等于0，是则执行步骤6.3)，否则将j的值减少1并继续执行步骤6.4)；6.5)将集合PS中的所有CSP进程并行组合起来且要求这些进程在事件B处同步，最终产生的CSP进程就是能够精确模拟执行路径p的等价通信行为的CSP模型Γ；6.6)输出CSP模型Γ。
2.根据权利要求1所述的结合符号执行和路径模型检验的MPI程序验证方法，其特征在于，步骤6.4)根据各个通信操作op j 的类型为其生成相应的CSP事件，具体按照如下类别处理：·针对类型为Ssend(i)的MPI通信操作op j 的处理步骤包括：为op j 分配一个唯一且大小为0的CSP管道c 1 ，往管道c 1 写入元素x来建模Ssend(i)；·针对类型为Send(i)和ISend(i,r)的MPI通信操作op j 的处理步骤包括：为op j 分配一个唯一且大小为1的CSP管道c 2 ，往管道c 2 写入元素x来建模Send(i)和ISend(i,r)；·针对类型为Barrier的MPI通信操作op j 的处理步骤包括：为op j 生成一个CSP同步事件B来建模Barrier；·针对类型为Recv(i)或Recv(*)的MPI通信操作op j 的处理步骤包括：首先通过静态匹配操作参数的方式获取通信操作op j 在路径p所产生的通信行为集合中能够匹配的发送操作所对应管道的集合C；然后使用CSP外部选择算子将集合C中所有管道的读操作进行组合；最后对外部选择组合模型进行精化，即如果集合C中的两个管道所对应的发送操作存在完成依赖关系，那么在管道读事件之前顺序拼接检查该管道所依赖管道是否为空的阻塞CSP事件；·针对类型为IRecv(i,r)或IRecv(*,r)的MPI通信操作op j 的处理步骤包括：先通过静态匹配操作参数的方式获取通信操作op j 在路径p所产生的通信行为集合中能够匹配发送操作所对应管道的集合C；然后使用CSP外部选择算子将集合C中所有管道的读操作进行组合；接着对外部选择组合模型进行精化，即如果集合C中的两个管道所对应的发送操作存在完成依赖关系，那么在管道读事件之前顺序拼接检查该管道所依赖管道是否为空的阻塞CSP事件；最后在精化后的CSP模型后顺序拼接上非阻塞接收操作的等待动作Wait所对应的CSP事件e w ；·针对类型为Wait(r)的MPI通信操作op j 的处理步骤包括：为op j 生成一个CSP事件e w 来建模Wait(r)，只对非阻塞接收对应的Wait(r)操作进行建模。
3.一种结合符号执行和路径模型检验的MPI程序验证系统，包括计算机设备，其特征在于，该计算机设备被编程以执行权利要求1或2所述结合符号执行和路径模型检验的MPI程序验证方法的步骤，或该计算机设备的存储介质上存储有被编程以执行权利要求1或2所述结合符号执行和路径模型检验的MPI程序验证方法的计算机程序。
4.一种计算机可读存储介质，其特征在于，该计算机可读存储介质上存储有被编程以执行权利要求1或2所述结合符号执行和路径模型检验的MPI程序验证方法的计算机程序。
