结合符号执行和路径模型检验的MPI程序验证方法、系统及介...
授权
摘要
本发明公开了一种结合符号执行和路径模型检验的MPI程序验证方法、系统及介质。本发明基于符号执行来系统遍历MPI程序的路径空间，在符号执行探索完一条正常终止路径p后，针对p的等价通信行为生成CSP模型Γ，然后使用模型检验来验证Γ是否满足给定性质若满足则裁剪符号执行探索路径p的过程中为通信行为的不同交叠执行情况和不同匹配情况所创建的待探索状态；否则找到违背性质
的反例并生成相应测试用例。当探索完MPI程序的路径空间、找到反例或超时，验证过程终止。本发明能对包含非阻塞和非确定性通信的实际MPI程序进行正确性验证，验证结果既能覆盖程序的输入空间又能覆盖进程的调度空间。
基本信息
专利标题 ：
结合符号执行和路径模型检验的MPI程序验证方法、系统及介质
专利标题（英）：
暂无
公开（公告）号 ：
CN110543353A
申请号 ：
CN201910837971.4
公开（公告）日 ：
2019-12-06
申请日 ：
2019-09-05
授权号 ：
CN110543353B
授权日 ：
2022-05-06
发明人 ：
于恒彪黄春王戟陈振邦傅先进彭林唐滔左克姜浩沈洁方建滨
申请人 ：
中国人民解放军国防科技大学
申请人地址 ：
湖南省长沙市开福区砚瓦池正街47号
代理机构 ：
湖南兆弘专利事务所(普通合伙)
代理人 ：
谭武艺
优先权 ：
CN201910837971.4
主分类号 ：
G06F9/48
IPC分类号 ：
G06F9/48 G06F9/445 G06F9/448
IPC结构图谱
G
G部——物理
G06
计算；推算或计数
G06F
电数字数据处理
G06F9/00
程序控制装置，例如，控制单元
G06F9/06
应用存入的程序的，即应用处理设备的内部存储来接收程序并保持程序的
G06F9/46
多道程序装置
G06F9/48
程序启动；程序切换，例如通过中断
法律状态
2022-05-06 ：
授权
2019-12-31 ：
实质审查的生效
IPC(主分类) : G06F 9/48
申请日 : 20190905
申请日 : 20190905
2019-12-06 ：
公开
注：本法律状态信息仅供参考，即时准确的法律状态信息须到国家知识产权局办理专利登记簿副本。
文件下载
暂无PDF文件可下载
