论文部分内容阅读
并发系统的模型是其性能评价、仿真、作业调度及控制的研究基础。互斥是并发系统最重要的性质之一。建立了具有互斥约束系统的一般数学模型——互斥模型。将模型互斥性分解为安全性、活性和无阻性约束，形式化规约成LTL公式；给出了基于不动点的互斥模型的模型检测算法。并结合实例进行了互斥模型的形式化验证。给出了模型精化改进的详细过程。随着并发系统进程增加。不动点模型检测算法会面临状态爆炸问题。给出了另一种基于布尔公式的BDD（二叉决策树）运算下的符号化模型检测方法．有效地缓解了状态爆炸问题。