基于Groebner基的模型检测技术及其工具实现

Model checking technology and tool development based on Groebner base

为了减少运算复杂度和运算时间,优化检测的性能,使得计算过程更加快速高效,在符号化模型检测的过程中,利用G roebner基进行多项式约化,设计出新的模型检测算法。并且基于该算法开发出新的符号模型检测工具。该工具能更快速地验证各软件及硬件系统的性质,具有较高的实用价值。

In this paper, a new model checking algorithm introduces the application of Groebner to reduce the polynomial formula in the property verification, and it can efficiently optimize the computing complexity problem. A new symbolic model checking tool was built based on this algorithm. And this tool is proved to be effective for different types of software and hardware system, and has high practice value.