基于常微分方程的程序死锁检测研究

状态空间爆炸问题是困扰程序分析领域几十年的问题。在对并发系统、分布式系统做静态分析时，系统中状态的数目会随着过程（或进程）的增加而呈指数级增长。本项目提出一种基于常微分方程的方法，在实际的程序死锁检测中，可以避开状态爆炸问题。.我们通过对离散系统的连续化，用常微分方程组来描述并发程序。其中每一个方程描述了一个事件引起程序状态的变化。线性化程序对应一组线性常微分方程。一个并发结构对应一组非线性常微分方程。程序状态可由0到1之间的数来度量。这个度量指出该状态在程序运行时能达到的程度。基于此，我们可以对程序性质进行分析。代之离散事件系统中穷举所有状态去分析程序的性质，我们可以通过分析常微分方程的解来得到。特别地，我们根据方程的解研究了程序有死锁的充分必要条件。对小型程序我们可由MATLAB解出所有的方程，并描出状态曲线。对大型程序，我们将开发出并行计算系统用于求解大规模非线性常微分方程组。