基于下推系统的GPU并行CTL模型检查方法

摘要

本发明公开了一种基于下推系统的GPU并行CTL模型检查方法，包括：将待验证的串行目标程序解析为下推系统；根据预设的CTL公式及下推系统，生成可交替布奇下推系统；采用图形处理器GPU并行技术，通过可交替自动机并行求解可交替布奇下推系统中所有被接收的下推系统格局；根据所有下推系统格局，验证串行目标程序是否满足CTL公式。本发明自动将串行的JAVA程序或C语言程序构建成下推系统，对CTL公式和下推系统进行叉乘，生成可交替布奇下推系统，利用GPU并行技术动态分配计算任务以适应单指令多数据流架构，求解所有可被自动机接收的格局。本发明可以高效地对下推系统进行空集分析和CTL模型检查，可以用于检查函数的调用过程分析及变量定义的时序性质分析。