科研之友
微信
新浪微博
Facebook
分享链接
摘要
本发明公开了一种基于下推系统的GPU并行CTL模型检查系统,包括：程序解析建模模块,用于将待验证的串行目标程序解析为下推系统；下推系统赋值模块,用于根据预设的CTL公式及下推系统,生成可交替布奇下推系统；并行CTL模型检查模块,用于采用图形处理器GPU并行技术,通过可交替自动机并行求解可交替布奇下推系统中所有被接收的下推系统格局；根据所有下推系统格局,验证串行目标程序是否满足CTL公式。本发明自动将串行目标程序构建成下推系统,对CTL公式和下推系统叉乘得到可交替布奇下推系统,利用GPU并行技术动态分配计算任务求解所有可被自动机接收的格局,能高效地对下推系统进行CTL模型检查,可用于函数的调用过程分析及变量定义的时序性质分析。
- 单位
