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

并发系统互斥约束的形式化验证＊ 鱼先锋1, 王辉2 （1. 商洛学院 计算机科学系 商洛 7260002; 2. 商洛学院 数学与计算科学系 商洛 726000） 摘要：并发系统的模型是其性能评价、仿真、作业调度及控制的研究基础. 互斥是并发系统最重要的性质之一，文章建立了具有互斥约束系统的一般数学模型——互斥模型. 将模型互斥性分解为安全性、活性和无阻性约束, 形式化规约成LTL公式; 给出了基于不动点的互斥模型的模型检测算法. 并结合实例进行了互斥模型的形式化验证, 给出了模型精化改进的详细过程. 随着并发系统进程增加, 不动点模型检测算法会面临状态爆炸问题, 文章给出了另一种基于布尔公式的BDD运算下的符号化模型检测方法, 算法简明高效, 有效的缓解了状态爆炸问题. 关键词：互斥模型 模型检测 不动点 BDD 中图法分类号: TP301 文献标识码: AFormal Verification of Mutex of concurrent system YU Xian-feng1，Wang Hui2 (1.Department of computer science, ShangLuo University, ShangLuo, 726000; 2.Department of mathematics and computer science, ShangLuo University, ShangLuo, 726000) Abstract: 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 paper establishes a general mathematical model—Mutex-Model for exclusive systems. Decomposes the mutex feature of concurrent system into safety, liveness and non-blocking and translates these features into LTL formulas formal specification. Gives a model checking algorithm based on fixpoint theory for Mutex-Model. And then combines with an example, the paper formally verifies the Mutex-Model . Gives the explicit refinement and improvement of the model. As concurrent system’s processes increase, this model checking algorithm have to face state explosion problem. So the paper gives another symbolic model checking algorithm based on BDD and Boolean formulas. This algorithm is simple and efficient, and effectively alleviate the state explosion problem. Keywords: Mutex-Model model checking fixpoint BDD 1. 互斥模型的形式化 在进程可以共享各类资源然而临界资源却是一次只能供一个进程使用使用完后归还系统才能给其他进程使用如Automatic Teller Machine)等. 该类系统要求进程对临界资源必须互斥使用为实现对临界资源的互斥访问，应保证进程互斥地进入自己的临界区为此每个进程在进入其临界区前必须先申请经允许后方能进入定义1（计算模型） 一个互斥模型为一个六元组, 其中, (1)为进程之集, 表示系统要处理的进程; (2) 赋值集, L中的元素表示进程所处的状态, 其中表示进程未没有占有临界资源，表示进程请求占有临界资源表示进程占有临界资源，其他元素的定义视不同系统实际需要而定; (3) 是有穷状态集合, ,即到的部分射; 表示第个进程所处的状态为, 记; (4