并发系统互斥约束的形式化验证

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

Formal Verification of Mutex of Concurrent System

The model of concurrent system is the research foundation of its performance evaluation, simulation, scheduling and control. Mutex is one of the most important features of concurrent systems. This study establishes a general mathematical model--Mutex-Model for exclusive systems.The mutex feature of concurrent system is decomposed into safety, liveness and non-blocking and these features are translated into LTL formulas formal specification. A model checking algorithm based on fixpoint theory for Mutex- Model is given. And then combined with an example,the paper formally verifies the Mutex-Model. The explicit refinement and improvement of the model is given. As concurrent system＇s processes increase, this model checking algorithm have to face state explosion problem. So another symbolic model checking algorithm based on BDD and Boolean formulas is proposed. This algorithm is simple and efficient, and effectively alleviate the state explosion problem.