《模型检测课程报告》由会员分享，可在线阅读，更多相关《模型检测课程报告（16页珍藏版）》请在金锄头文库上搜索。
1、北京工业大学 2020-2021 学年第一学期模型检测课程实验报告院系：信息学部姓名：李昌树学号：S202074014指导老师： 李童完成时间： 2020.1112目录1 背景介绍 12 问题描述 12.1 哲学家用餐问题 12.2 实验假设 22.3 建模 22.3.1 哲学家 22.3.2 筷子 23 Spin 模型检测工具 33.1 Spin 的使用 33.2 模型代码 33.3 代码说明 53.4 检测结果 53.5 结果分析 84 添加约束规则 84.1 规则 84.2 代码（核心代码） 84.3 检测结果 94.4 饥饿现象分析 114.5 解决饥饿 115 实验总结 121背景介
2、绍哲学家用餐问题是在计算机科学中的一个经典问题,用来演示在并行计算中多线程同步 (Sy nchro nizatio n)时产生的问题。在1971年，著名的计算机科学家艾兹格迪科斯彻提出 了一个同步问题，即假设有五台计算机都试图访问五份共享的磁带驱动器。稍后，这个问 题被托尼霍尔重新表述为哲学家用餐问题。这个问题可以用来解释死锁和资源耗尽。2问题描述2.1 哲学家用餐问题假设有一群哲学家，他们的生活只有思考和吃饭。现在这些哲学家共用一个餐桌，每位 都有一个座位，桌子中央有有一大碗米饭，桌子边缘按顺序摆放着数量与哲学家数量相同 的筷子。他们从不与其他人交流，当一位哲学家思考完后感到饥饿时，就会试图
3、拿起左右 两边的筷子，但一次只能拿一根筷子，且不能从别人手里拿筷子，当拿到一双筷子后，他 就可以开始吃饭了，吃完后，他会放下两根筷子，并开始思考。如图1所示。图 1. 哲学家用餐问题2.2 实验假设假设现在有5个哲学家和5 根筷子，它们的编号都是0至4。哲学家们的初始状态都是 思考，他们左右手两边各有一根筷子。当其中一位哲学家思考一段时间后，他们会感到饥 饿，随后就会尝试拿起左右两边的筷子，当得到一双筷子之后，他就会开始用餐，用餐完 毕后就会进入思考状态，他们处于这样的循环中。如图2 所示。图 2 哲学家状态变迁图2.3 建模使用符号来表示哲学家，筷子，以及它们的状态变迁。2.3.1 哲学家定
4、义5个哲学家，并用X。表示哲学家进入思考状态，X1表示哲学家进入饥饿状态，X2 表示哲学家进入用餐状态。那么他们的状态变迁就只能为(X0-X), “-込)，(X2-X0)。需要 注意的是(X-X2)这个过程必须要满足一定的条件才可以发生。2.3.2 筷子定义一个筷子数组，长度为5，存储的是数字变量，初始为空闲状态，表示为-1。当一 根筷子被哲学家占有时，这根筷子的所对应的值为这个哲学家的编号，但必须注意的是，哲学家的只能拿起他左右两边的筷子，而不能去拿别人左右两边的筷子，也就是说每一根筷子的状态最多有3个。下面用f表示筷子，后面的数字表示筷子的编号，括号中的量表 示为筷子可能的状态。f0: （
5、-1， 0， 1）f1: （-1，1，2）f2: （-1，2，3）f3: （-1，3，4）f4: （-1，4，0）很容易得出，筷子的状态有35 种。3 Spin模型检测工具这个工具的不仅使用需要一定的理论基础，就连安装也有一定的门槛，我在国庆期间话 费了大量时间才安装的差不多，但仍有一个出图的功能没有安装完毕，我已经将自己总结 的安装步骤放在了我的博客上 https:/ 的使用Spin检测模型时，主要分为三块，safety、liveness、以及LTL never claims。3.2 模型代码#define NUM_PHIL 5bool pthinkingNUM_PHIL , phungry
6、NUM_PHIL, peatingNUM_PHIL=false;int forksNUM_PHIL=-1;proctype philosopher（ int i ） int right=i;int left=(i+1)%NUM_PHIL;Think : atomic peatingi=false;pthinkingi=true ; ; /*Nothing*/Hungry:atomicpthinkingi=false;phungryi=true; if:skip;atomicforksleft=-1-forksleft=i;atomicforksright=-1-forksright=i;:sk
7、ip;atomicforksright=-1-forksright=i; atomicforksleft=-1-forksleft=i;fi;Eating:atomicphungryi=false;peatingi=true;Done:forksright=-1;forksleft=-1goto Think;initint philosophers=NUM_PHIL-1;atomicdo:(philosophers0) -philosophers-;run philosopher(philosophers);:(philosophers=0) -breakod#define p philoso
8、pher0Eating #define q philosopher1Eatingltl c1pltl c2pltl c3(p-q)ltl c4( forks0=0& forks1=1& forks2=2& forks3=3& forks4=4)3.3代码说明.pthinking数组，phungry数组，peating数组的长度与哲学家的数量一致，这里面存储 的都是布尔变量，使用它们来表示每一位哲学家此时的状态。如thinking0=true,说 明此时编号为0的哲学家处于思考状态。后面的同理。forks 数组的作用上文已经介绍，此处不再赘述。. 很容易得出，编号为i的哲学家拿筷子的动作可以表示
9、为forksleft=-1-forksleft=i, forksright=-1-forksright=i。我将这两条语句都定义为了原语。. 代码结尾处的LTL表达式，C1:编号为0的哲学家可以用上餐一一Fp； c2:编号为0的哲 学家可以始终用上餐(Infinity Often)GFp； c3:如果编号为0的哲学家能用上餐，那么编号为1的哲学家也一定能用上餐一一F(p-q)；c4:检验是否会出现每一根筷子都被 不同的哲学家所占有，即死锁状态。3.4 检测结果1. 语法检测，如图，没有错误2. 由 spin 生成的状态变迁图Sr rn_ 門uii叨讥 pll|nkingi= pUiiiiki
10、打 i | =ph隔川=I萼 rtihLeM=f 肝rihl |=-i_連)lurlor|cKlefl = iEo|csri s-ht = iSLf；H)悴 left? = pj51K-irJzs| rii：hL4=i=tHirjill l =-1plmnjiryri=)pcti呱i = I3. 在 Verification 分栏中测试代码测试结果：spin -a phi losophsr. pm IIt I cl: ( (ph i I osopher M at i nff)111 c2: LJ (phi losopher 0QEating)Itl c3: j ( (phi Iosopharo
11、-Eating)(O (phi losopherlllSEaTingi1)Itl c4- C(-fwksrol=O)駆(fGrk9ni=l)D 眺(forks21=2)1)应(forksr31=3) 8* (forks41 =4) the mode I oonta i ns -4 newer elm inns: cdr c3r c2, c1only ww 4lAlm Is used In a verificatim runchoose which one with . /prn -a -N man橹 Cdefaiilts to -N -oilor use e. g : sp i n searc
12、h -l 11 d phi lasopher pailgee DMEMLIH二P24 -02 -DXUSAFE r -o pan pan. c./gn -mIOCflO 一b -N dPidl: 1I65C-pan: Itl formula Zpsrv1: B&eeptan&e 仍role： hkpMSC: G line 4_1 :proc - tl :1) _spin_ni/r. Imp:4 (state 11) (I (phi losoph&r Lfl, _p=Eat ing)Never claim moves to I i ne 4 . (.! (ph I &soph&r0.Eat i ng) _2:proc0(:i nit:1)philosoph&r. pm 1:312:proc0(:init:1)philosoph&r.pml:32Start ing phi losoph&r with pid 23;proc0(: i nit: 1)phiIosoph&r. pnil: 334:proc0(:i nit:1)philosoph&r. pm 1:314:proc0(
