资源描述：
《并发系统互斥约束的形式化验证》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、并发系统互斥约束的形式化验证＊鱼先锋1,王辉2（1.商洛学院计算机科学系商洛7260002;2.商洛学院数学与计算科学系商洛726000）摘要：并发系统的模型是其性能评价、仿真、作业调度及控制的研究基础.互斥是并发系统最重要的性质之一，文章建立了具有互斥约束系统的一般数学模型——互斥模型.将模型互斥性分解为安全性、活性和无阻性约束,形式化规约成LTL公式;给出了基于不动点的互斥模型的模型检测算法.并结合实例进行了互斥模型的形式化验证,给出了模型精化改进的详细过程.随着并发系统进程增加,不动点模型检测算法会面临状态
2、爆炸问题,文章给出了另一种基于布尔公式的BDD运算下的符号化模型检测方法,算法简明高效,有效的缓解了状态爆炸问题.关键词：互斥模型模型检测不动点BDD中图法分类号:TP301文献标识码:AFormalVerificationofMutexofconcurrentsystemYUXian-feng1，WangHui2(1.Departmentofcomputerscience,ShangLuoUniversity,ShangLuo,726000;2.Departmentofmathematicsandcompute
3、rscience,ShangLuoUniversity,ShangLuo,726000)Abstract:Themodelofconcurrentsystemistheresearchfoundationofitsperformanceevaluation,simulation,schedulingandcontrol.Mutexisoneofthemostimportantfeaturesofconcurrentsystems.Thispaperestablishesageneralmathematicalmo
4、del—Mutex-Modelforexclusivesystems.Decomposesthemutexfeatureofconcurrentsystemintosafety,livenessandnon-blockingandtranslatesthesefeaturesintoLTLformulasformalspecification.GivesamodelcheckingalgorithmbasedonfixpointtheoryforMutex-Model.Andthencombineswithane
5、xample,thepaperformallyverifiestheMutex-Model.Givestheexplicitrefinementandimprovementofthemodel.Asconcurrentsystem’sprocessesincrease,thismodelcheckingalgorithmhavetofacestateexplosionproblem.SothepapergivesanothersymbolicmodelcheckingalgorithmbasedonBDDandB
6、ooleanformulas.Thisalgorithmissimpleandefficient,andeffectivelyalleviatethestateexplosionproblem.Keywords:Mutex-ModelmodelcheckingfixpointBDD1.互斥模型的形式化在并发系统中进程可以共享各类资源,然而临界资源却是一次只能供一个进程使用,使用完后归还系统,才能给其他进程使用.如网络打印机、ATM(AutomaticTellerMachine)等.该类系统要求进程对临界资源必须互
7、斥使用,为实现对临界资源的互斥访问，应保证各个进程互斥地进入自己的临界区,称为安全性约束.为此,每个进程在进入其临界区前,必须先申请,经允许后方能进入.为了体现公平性,各个进程都可以申请占有临界资源,这是无阻性约束,且一但申请最终将占有临界资源,此为活性约束.下面给出互斥模型的形式化定义.定义1（计算模型）一个互斥模型为一个六元组,其中,(1)为进程之集,表示系统要处理的进程;＊项目基金：商洛学院科研基金项目10SKY023；作者简介：鱼先锋(1984—),男,助教,硕士研究生,研究方向:模型检测,Email:p
8、ioneer.369@163.com;王辉(1979—),男,讲师,硕士研究生,研究方向:模糊数学,Email:wangh828@163.com.(2)赋值集,L中的元素表示进程所处的状态,其中表示进程未没有占有临界资源，表示进程请求占有临界资源,表示进程占有临界资源，其他元素的定义视不同系统实际需要而定;(3)是有穷状态集合,,即到的部分映射;,表示第个进程所处的状态为
