基于基本并发进程的异步通讯程序的验证模型与高效算法

The current existing methodology for verification problem of asynchronously communicating programs is to reduce to the computations on Petri nets. The complexity is high, and there is no systematic theoretical results and efficient verification tools yet. We found that the programs can be reduced to the computations on basic parallel processes (BPP), and the theoretical complexity is greatly reduced. To this end, it is intended to carry out the systematic research on the programs based on BPP, through the classification of communications, for weakly communicating programs and strongly communicating programs, including: 1) For the weakly communicating programs, the stacks are adopted for a variety of nontrivial approximations, and investigate their complexity results for the safety and liveness problems; 2) For the strongly communicating programs, communications and stacks are adopted respectively regular pattern approximations, by adding a variety of program features, and investigate the decidability and complexity of theirs safety and liveness problems. 3) Implement the BPP bounded model checker based on SMT solver, perform detailed research on the liveness of the programs, investigate the corresponding decidable verification property on BPP, and complete the efficient algorithms of encoding from different asynchronously communicating programs to BPP. Through the above researches, we can get the decidability and complexity results of the asynchronously communicating programs under different approximation conditions systematically and comprehensively, and develop an efficient verification tool.

目前异步通讯程序的验证方法是通过将其归约到Petri网上的计算，复杂性高且尚未有系统性的理论结果和高效工具。我们发现此类程序的验证方法可以归约到基本并发进程（BPP）上的计算，从而复杂性大大降低。本项目在前期研究基础上，拟通过对程序的通讯进行分类，将其分为弱通讯程序和强通讯程序，并且基于BPP分别对其展开系统性研究。包括：1）对弱通讯程序的栈进行多种非平凡的近似，研究安全性和活性的复杂性问题；2）对强通讯程序的输入通讯和栈分别进行正则模式近似，并且加入多种程序特性，研究其安全性和活性的判定性和复杂性问题。3）研究实现基于SMT求解器的BPP限界模型检测器，并且对程序的活性进行细粒度的研究，得到BPP上对应的可判定的验证性质，并且完成从不同种异步通讯程序到BPP编码的高效算法。通过上述研究，可系统全面地得到异步通讯程序在不同近似条件下的验证问题的判定性和复杂性结论，并开发出高效的验证工具。

目前异步通讯程序的验证方法是通过将其归约到Petri网上的计算，复杂性高且尚未有系统性的理论结果和高效工具。我们发现此类程序的验证方法可以归约到基本并发进程（BPP）上的计算，从而复杂性大大降低。本项目在前期研究基础上，拟通过对程序的通讯进行分类，将其分为弱通讯程序和强通讯程序，并且基于BPP分别对其展开系统性研究。包括：1）对弱通讯程序的栈进行多种非平凡的近似，研究安全性和活性的复杂性问题；2）对强通讯程序的输入通讯和栈分别进行正则模式近似，并且加入多种程序特性，研究其安全性和活性的判定性和复杂性问题，并且实现了Erlang语言的程序验证工具Ramble；3）研究实现基于SMT求解器的BPP限界模型检测器BPPChecker，并且对程序的活性进行细粒度的研究，得到BPP上对应的可判定的验证性质，并且完成从不同种异步通讯程序到BPP编码的高效算法。通过上述研究，可系统全面地得到异步通讯程序在不同近似条件下的验证问题的判定性和复杂性结论，并开发出高效的验证工具。