模拟试题 《软件形式化方法》期末考试试题 (120分钟) 题号 四五六七总分 题分 得分 、填空题。(20分) 1.软件开发是一项包括需求获取、 系统实现、测试的系统工程,主 要经历了三个发展阶段 2.现代软件工程对于软件的定义中包括:当它被执行时能够提供所要求的功能和性能 的的 使得程序能够满意地处理信息的」 描述程序的功能需求以及程序 软件工程的目标是成功地生产具有 及开销合宜的产品。 3.在形式化方法框架内可以以系统的方式 系统;软件开发中的形 式化方法主要运用 描述“需求的清晰陈述”。 4.VDM是一种功能性规格说明技术,通过 和已建立的 来描述每个运算或函数 的功能:与Z语言类似,VDM中的集合表示方法有 对一个软件系统来说 其ⅴDM描述包括 和 两个部分。 二、对于图中所示有限状态机的状态转移图,给出其关系矩阵和状态转移表。(10分) 三、简述 Petri网中的顺序关系、并发关系、冲突关系和混惑关系。(10分) 四、计算下列进程的事件集和迹。(10分) (P1)μX:{a,b}·a→X (P2)(a→STOP{ab)b→STOP{ab;) 五、逻辑演算证明。(15分) (1)(P∧Q)∧R上PA(Q∧R) (2)F(P→(Q→R)…(P∧Q)→R) (3)P(a, b)A(VX)(y)P(Y, X)VP(X, Y)-P(X, X))+P(a, a 六、对于图中所示的 Kripke结构,写出其对应的三元组形式,并分别在状态so,sl,s2 s3下考察下述CTL公式是否成立。(20) (1) EOp (2)Ap (3)E(Ep)
模拟试题一 《软件形式化方法》期末考试试题 （120 分钟） 题号 一 二 三 四 五 六 七 总分 题分 得分 一、填空题。（20 分） 1. 软件开发是一项包括需求获取、 、 、系统实现、测试的系统工程，主 要经历了三个发展阶段： 、 、 。 2. 现代软件工程对于软件的定义中包括：当它被执行时能够提供所要求的功能和性能 的 ；使得程序能够满意地处理信息的 ；描述程序的功能需求以及程序 的 。软件工程的目标是成功地生产具有 、 及开销合宜的产品。 3. 在形式化方法框架内可以以系统的方式 、 和 系统；软件开发中的形 式化方法主要运用 和 描述“需求的清晰陈述”。 4. VDM 是一种功能性规格说明技术，通过 和已建立的 来描述每个运算或函数 的功能；与 Z 语言类似，VDM 中的集合表示方法有 和 ；对一个软件系统来说， 其 VDM 描述包括 和 两个部分。 二、对于图中所示有限状态机的状态转移图，给出其关系矩阵和状态转移表。（10 分） 三、简述 Petri 网中的顺序关系、并发关系、冲突关系和混惑关系。（10 分） 四、计算下列进程的事件集和迹。（10 分） (P1) μX: {a, b} ·a→X (P2) (a→STOP{a, b})||(b→STOP{a, b}) 五、逻辑演算证明。（15 分） （1）(P∧Q) ∧R├ P∧(Q∧R) （2）├ (P→(Q→R)) ↔ ((P∧Q) →R) （3）P(a, b) ∧(X)( (y)P(Y, X) ∨P(X, Y) →P(X, X)) ├P(a, a) 六、对于图中所示的 Kripke 结构，写出其对应的三元组形式，并分别在状态 s0，s1，s2， s3 下考察下述 CTL 公式是否成立。（20） （1）E○p （2）Ap （3）E◊(Ep)
七、对于某互联网应用系统,每个用户使用系统前必须用口令进行登录。应用Z语言规格 个系统 LogSys,该系统可以保存已注册的用户及其口令信息,并且可以跟踪当前已登录 系统的在线用户。(15) (1)定义△ LogSys、三 LogSys和 InitLogSys: (2)定义操作模式,用来注册一个新的用户和口令 (3)定义操作模式,用来注销一个用户及其口令
七、对于某互联网应用系统，每个用户使用系统前必须用口令进行登录。应用 Z 语言规格 一个系统 LogSys，该系统可以保存已注册的用户及其口令信息，并且可以跟踪当前已登录 系统的在线用户。（15） （1）定义ΔLogSys、ΞLogSys 和 InitLogSys； （2）定义操作模式，用来注册一个新的用户和口令； （3）定义操作模式，用来注销一个用户及其口令
参考答案与答题要点 、填空题 1.需求分析系统设计程序设计阶段程序系统阶段 2.指令或计算机程序数据结构操作和使用文档正确性可用性 3.刻画开发验证集合论逻辑符号体系 4.一阶谓词逻辑抽象数据类型枚举表示法特征表示法状态操作 二、状态转移图和状态转移表 状态,输入 0 qqq 三、M为Peri网EN的一个标识,若存在t和使得M[tl>M,且Mt>,M[2 亦即,在M标识下,t1使能,而t2不使能,且t的引发会使使能,即t的使能以 tl的引发为条件,则称t和t2在M下有顺序关系 M为Peti网PN的一个标识,若存在t和t2使得M[tl>和M[t2>,并满足M[tl>Ml MI[t>,且M[t2M2→M2[tl>,则称t和?在M下并发。就是说M标识下,tl 和口都使能,且它们当中任一个迁移的引发都不会使另一个迁移不使能 M为Pet网PN的一个标识,若存在t和t2使得M[t>和Mt2>,并满足Mtl>Ml→ M1[t>,且Mt2M→M[tl>,则称tl和在M下冲突。就是说M标识下, tl和口都使能,但它们当中任一个迁移的引发都会使另一个迁移不使能。 个Peti网中可能同时存在着并发和冲突,而且并发迁移的引发会引起冲突的消失 或出现。像这样并发和冲突混合在一起产生的困惑,无法根据状态的变化判断其间是否 出现过冲突,所以将这种情况称为混惑 四、(P1)事件集:{a,b} 迹:{<>,,,,} 五、(1)(P∧Q∧R卜P∧(Q∧R) 1.P∧Q 前提引入规则 1及基本蕴含公式 3.Q 1及基本蕴含公式 前提引入规则 5.Q∧R 3,4及基本蕴含公式 6.P∧(Q∧R) 2,5及基本蕴含公式 (2)卜(P-(Q→R)+(P∧Q)→R) 前提引入规则 2. PV(Q 1及基本等价公式 3.-PV(_Q∨R) 2及基本等价公式 4._P∨-QVR 3及基本等价公式
参考答案与答题要点 一、填空题 1. 需求分析 系统设计 程序设计阶段 程序系统阶段 2. 指令或计算机程序 数据结构 操作和使用文档 正确性 可用性 3. 刻画 开发 验证 集合论 逻辑符号体系 4. 一阶谓词逻辑 抽象数据类型 枚举表示法 特征表示法 状态 操作 二、状态转移图和状态转移表 三、M 为 Petri 网 PN 的一个标识，若存在 t1 和 t2 使得 M[ t1>M’，且﹁M[ t2>，M’[ t2>， 亦即，在 M 标识下，t1 使能，而 t2 不使能，且 t1 的引发会使 t2 使能，即 t2 的使能以 t1 的引发为条件，则称 t1 和 t2 在 M 下有顺序关系。 M为Petri网PN的一个标识，若存在t1 和t2 使得M[ t1>和M[t2>，并满足M[ t1>M1=> M1 [ t2>，且 M[ t2>M2=> M2[t1>， 则称 t1 和 t2 在 M 下并发。就是说 M 标识下，t1 和 t2 都使能，且它们当中任一个迁移的引发都不会使另一个迁移不使能。 M为Petri网PN的一个标识，若存在t1 和t2 使得M[ t1>和M[t2>，并满足M[ t1>M1=> ﹁M1 [ t2>，且 M[ t2>M2=> ﹁M2[t1>， 则称 t1 和 t2 在 M 下冲突。就是说 M 标识下， t1 和 t2 都使能，但它们当中任一个迁移的引发都会使另一个迁移不使能。 一个 Petri 网中可能同时存在着并发和冲突，而且并发迁移的引发会引起冲突的消失 或出现。像这样并发和冲突混合在一起产生的困惑，无法根据状态的变化判断其间是否 出现过冲突，所以将这种情况称为混惑。 四、(P1) 事件集：{a, b} 迹：{, , , , …} (P2) 事件集：{a, b} 迹：{, , } 五、（1）(P∧Q) ∧R├ P∧(Q∧R) 1. P∧Q 前提引入规则 2. P 1 及基本蕴含公式 3. Q 1 及基本蕴含公式 4. R 前提引入规则 5. Q∧R 3,4 及基本蕴含公式 6. P∧(Q∧R) 2,5 及基本蕴含公式 （2）├ (P→(Q→R)) ↔ ((P∧Q) →R) 1. P→(Q→R) 前提引入规则 2. P∨(Q→R) 1 及基本等价公式 3. P∨(Q∨R) 2 及基本等价公式 4. P∨Q∨R 3 及基本等价公式
5._(P∧QVR 4及基本等价公式 6.(P∧Q→R 5及基本等价公式 (3)P(ab)∧X(y)P(YX)VPXY)→P(X2Ⅹ)}P(aa 合取因子:P(a,b)-P(y,x)VP(x,x),-P(x,y)VP(x,x)-P(aa) 1. P(x, y)VP(x, X) 前提引入规则 2.-P(ab)VP(a,a)1及全称量词消去规则 3.-P(a,a) 前提引入规则 4.-P(a 3及基本等价公式 5.P(a,b) 前提引入规则 6. NIL 4,5归结 六、W={a0,s1,s2,s3}R={,,,,,} L(S0)={p},Lsl)={pq},L(s2)={p,r},L(s3)={q} EOp:s0sls2成立s3不成立 Ap.s0sls2s3均不成立 E(Ep):s0sls2成立s3不成立 七、模式定义 registry, registry: P User login, login: P User login registry login'Cregistr ---------8 LogSys- △ LogSys registry= registry login= login InitLogSys----------- registry: P User password? seq Char registry=registry U ( name? oo password? login’=ogin
5. (P∧Q)∨R 4 及基本等价公式 6. (P∧Q) →R 5 及基本等价公式 （3）P(a, b) ∧(X)( (y)P(Y, X) ∨P(X, Y) →P(X, X)) ├P(a, a) 合取因子：P(a, b) P(y, x)∨P(x, x), P(x, y)∨P(x, x) P(a, a) 1. P(x, y)∨P(x, x) 前提引入规则 2. P(a, b)∨P(a, a) 1 及全称量词消去规则 3. P(a, a) 前提引入规则 4. P(a, b) 3 及基本等价公式 5. P(a, b) 前提引入规则 6. NIL 4,5 归结 六 、 W={a0, s1, s2, s3} R={, , , , , } L(s0)={p}， L(s1)={p,q}， L(s2)={p,r}，L(s3)={q} E○p: s0 s1 s2 成立 s3 不成立 Ap: s0 s1 s2 s3 均不成立 E◊(Ep): s0 s1 s2 成立 s3 不成立 七、模式定义: （1） ---------ΔLogSys---------------- registry, registry’ : P User login, login’: P User --------------------------------------------- login⊆registry login’⊆registry’ ---------------------------------------------- ---------ΞLogSys---------------- ΔLogSys --------------------------------------------- registry= registry’ login= login’ --------------------------------------------- ---------InitLogSys---------------- registry’ : P User login’: P User --------------------------------------------- registry’={ } login’={ } --------------------------------------------- （2） ---------RegistrySys--------------------- ΔLogSys name?: seq Char password?: seq Char --------------------------------------------- registry’= registry∪{name? password?} login’=login --------------------------------------------- （3）
LogoutSys-- name?: seq Char login=(name) < login 模拟试题二 《软件形式化方法》期末考试试题 (120分钟) 题 三|三四五六七总分 得分 、填空题。(20分) 1.软件危机是指在计算机软件的开发和维护过程中所遇到的一系列严重的问题,其产生的 原因主要包括: 其本质特征是软件的 2.形式化方法研究如何把(具有淸晰数学基础的)严格性(描述形式、技术和过程等)融 入软件开发的各个阶段:包括形式化规格、 三种活动,在软件开发的形式化 规格中包含的三种规格为 3. Petri网适合于描述并发、异步、分布式软件系统规格,是由 和 个部分组成:特殊的 Petri网类型中, 不能描述冲突 允许冲突和并 发同时存在 可以用来描述非对称类型的混惑关系 4.模式是Z语言规格中一个重要的元素,模式包含和模式连接的前提条件是—,即不 同模式中 是相同的。 二、构造有限状态机,使其接受的语言为由0和1构成的字符串的集合,分别满足下列条件 (10分) (1)每个字符串以00结束 (2)每个字符串中有3个连续的0出现 三、对图中所示 Petri网进行化简。(10分) 四、构造下述系统过程的CSP进程。(10分) 银行的每个客户先开设(open)一个账户,然后该客户就可以多次执行存( deposit)或 取( withdraw)操作,最终还可能终止( terminate)该账户。假定不考虑客户每次存或取得 款项数目,也不考虑透支的情况 五、逻辑演算证明。(15分) (1)(PVQ)∧(PVR)P∨(Q∧R) (2)P∧(Q4R)}(P∧Q)(P∧R) (3)F(3xP(x)→(Y)P(Y) 六、对于图中所示的 Kripke结构,写出其对应的三元组形式,并分别在状态so,sl,s2 3下考察下述CTL公式是否成立。(20) (1)AOp (2)Ep
---------LogoutSys----------------------- ΔLogSys name?: seq Char --------------------------------------------- login’= {name} login --------------------------------------------- 模拟试题二 《软件形式化方法》期末考试试题 （120 分钟） 题号 一 二 三 四 五 六 七 总分 题分 得分 一、填空题。（20 分） 1. 软件危机是指在计算机软件的开发和维护过程中所遇到的一系列严重的问题，其产生的 原因主要包括： 、 、 、 ；其本质特征是软件的 和 。 2. 形式化方法研究如何把（具有清晰数学基础的）严格性（描述形式、技术和过程等）融 入软件开发的各个阶段；包括形式化规格、 和 三种活动，在软件开发的形式化 规格中包含的三种规格为 、 和 。 3. Petri 网适合于描述并发、异步、分布式软件系统规格，是由 、 和 三 个部分组成；特殊的 Petri 网类型中， 和 不能描述冲突， 允许冲突和并 发同时存在， 可以用来描述非对称类型的混惑关系。 4. 模式是 Z 语言规格中一个重要的元素，模式包含和模式连接的前提条件是 ，即不 同模式中 是相同的。 二、构造有限状态机，使其接受的语言为由 0 和 1 构成的字符串的集合，分别满足下列条件。 （10 分） （1）每个字符串以 00 结束。 （2）每个字符串中有 3 个连续的 0 出现。 三、对图中所示 Petri 网进行化简。（10 分） 四、构造下述系统过程的 CSP 进程。（10 分） 银行的每个客户先开设（open）一个账户，然后该客户就可以多次执行存（deposit）或 取（withdraw）操作，最终还可能终止（terminate）该账户。假定不考虑客户每次存或取得 款项数目，也不考虑透支的情况。 五、逻辑演算证明。（15 分） （1）(P∨Q) ∧(P∨R)├ P∨ (Q∧R) （2）P∧(Q↔R)├ (P∧Q) ↔(P∧R) （3）├ (x)(P(X) →(Y)P(Y)) 六、对于图中所示的 Kripke 结构，写出其对应的三元组形式，并分别在状态 s0，s1，s2， s3 下考察下述 CTL 公式是否成立。（20） （1）A○p （2）Ep
(3)A(p>q) 七、在教材7、3节中描述的电话号码系统中增加下列操作,给出完整的操作模式。(15) (1)收回电话( RemoveEntry):收回已经分配给某人的电话 (2)查询电话用户( FindNames):查询指定号码的电话用户; (3)更改电话号码( ChangeEntry):更改某个用户的电话号码
（3）A(p▷q) 七、在教材 7.3 节中描述的电话号码系统中增加下列操作，给出完整的操作模式。（15） （1）收回电话（RemoveEntry）：收回已经分配给某人的电话； （2）查询电话用户（FindNames）：查询指定号码的电话用户； （3）更改电话号码（ChangeEntry）：更改某个用户的电话号码
参考答案与答题要点 、填空题 1.软件开发成本高速度缓慢甚至延迟软件运行的质量差可靠性难以得到保证复杂 性多样性 2.形式化验证程序精化行为规格设计规格程序规格 3.位置迁移流关系状态机标记图自由选择网非对称的自由选择网 4.模式兼容同一变量的类型 ..@ (1) (2) 四、BANK=pen->(x:{ deposit, withdraw}→OPER(x)→ terminate OPER(deposit F(deposit->STOP) OPER(withdraw =(withdraw->STOP) 五、(1)(PVQ)∧ (PVRI P V(Q∧R) 1. PVQ 前提引入规则 2.P∨R 前提引入规则 3.P(Q∧R) 1,2及基本蕴含公式 (2)P∧(Q4→R)(P∧Q←(PAR) 1.Q+R 前提引入规则 2.(Q∧R)∨(Q∧=R) 1及基本等价公式 3.(QVR)∧(QVR) 2及基本等价公式 4.P,-QVR,Q∨→R 3及前提引入规则 Q 假设前提引入 5及基本蕴含公式
参考答案与答题要点 一、填空题 1. 软件开发成本高 速度缓慢甚至延迟 软件运行的质量差 可靠性难以得到保证 复杂 性 多样性 2. 形式化验证 程序精化 行为规格 设计规格 程序规格 3. 位置 迁移 流关系 状态机 标记图 自由选择网 非对称的自由选择网 4. 模式兼容 同一变量的类型 二、 （1） （2） 三、 （1） （2） 四、 BANK=open->(x:{deposit, withdraw}→OPER(x))→terminate; OPER(deposit)=(deposit→STOP); OPER(withdraw)=(withdraw→STOP)。 五、（1）(P∨Q) ∧(P∨R)├ P∨ (Q∧R) 1. P∨Q 前提引入规则 2. P∨R 前提引入规则 3. P∨ (Q∧R) 1,2 及基本蕴含公式 （2）P∧(Q↔R)├ (P∧Q) ↔(P∧R) 1. Q↔R 前提引入规则 2. (Q∧R)∨(¬Q∧¬ R) 1 及基本等价公式 3. (¬Q∨R) ∧(Q∨¬ R) 2 及基本等价公式 4. P, ¬Q∨R, Q∨¬ R 3 及前提引入规则 5. P∧Q 假设前提引入 6. Q 5 及基本蕴含公式
4.6及基本蕴含公式 8.P∧R 4,7及基本蕴含公式 9.(P∧Q→(P∧R) 58归结 10.P∧R 假设前提引入 10及基本蕴含公式 4,11及基本蕴含公式 13.P∧Q 4,12及基本蕴含公式 14.(P∧R)→(P∧Q) 5,8归结 15.(P∧Q)+(P∧R) 9,14归结 (3)(Bx)P(X)→(YP(Y) 1.(3x)(P(X)一(VYP(Y) 前提引入规则 2.-(彐x)P(X)∨(Y)P(Y) 1及基本蕴含规则 3.(x)-P(X)V(vYP(Y)2及量词转换规则 4.(VX)(P(X)VP(X)) 3及全称量词消除规则 5.-P(a)P(a) 4及全称量词消除规则 6.T 5及基本等价公式 六、W={a0,sl,s2,s3}R={,,,,, L(S0)={p},Lsl)={pq},L(s2)={pr},L(s3)={q} AOp:s0,s2成立sl,s3不成立 Ep:s0,sl1,s2成立s3不成立 A(pDq):s0,sl1,s2,s成立 七、模式定义 Remove Entry △ PhoneD name? Person name?∈ dom hasphone FindNames----------. =PhoneD name!=hasphone:(I()D
7. R 4,6 及基本蕴含公式 8. P∧R 4,7 及基本蕴含公式 9. (P∧Q) →(P∧R) 5,8 归结 10. P∧R 假设前提引入 11. R 10 及基本蕴含公式 12. Q 4,11 及基本蕴含公式 13. P∧Q 4,12 及基本蕴含公式 14. (P∧R) →(P∧Q) 5,8 归结 15. (P∧Q) ↔(P∧R) 9,14 归结 （3）├ (x)(P(X) →(Y)P(Y)) 1. (x)(P(X) →(Y)P(Y)) 前提引入规则 2. ¬(x)P(X)∨(Y)P(Y) 1 及基本蕴含规则 3. (x) ¬P(X)∨(Y)P(Y) 2 及量词转换规则 4. (x) (¬P(X)∨P(X)) 3 及全称量词消除规则 5. ¬P(a)∨P(a) 4 及全称量词消除规则 6. T 5 及基本等价公式 六 、 W={a0, s1, s2, s3} R={, , , , , } L(s0)={p}， L(s1)={p,q}， L(s2)={p,r}，L(s3)={q} A○p：s0, s2 成立 s1, s3 不成立 Ep ：s0, s1, s2 成立 s3 不成立 A(p▷q)：s0, s1, s2, s4 成立 七、模式定义: （1） ---------RemoveEntry---------------- ∆PhoneDB name?: Person --------------------------------------------- name? ∈dom hasphone hasphone’= {name?} hasphone --------------------------------------------------------- （2） ---------FindNames---------------- =PhoneDB number?: Phone --------------------------------------------- number? ∈ran hasphone name!= hasphone-1 (|{number}|)
(3) Change Entry- △ PhoneD name?: Person newnumber? Phone nane?∈ dom hasphone hasphone'=((name? hasphone)U(name? oonewnumber 模拟试题三 《软件形式化方法》期末考试试题 (120分钟) 题号 二|三四五六七总分 题分 得分 、填空题。(20分) 1.软件危机是指在计算机软件的过程中所遇到的一系列严重的问题,应对软件危机 的方式分为两种方法: 和 对于软件开发组织和管理的规范化方法中,主要研 究 2.形式化方法研究如何把(具有清晰数学基础的) (描述形式、技术和过程等) 融入软件开发的各个阶段;包括 形式化验证和程序精化三种活动。形式化验证主 要技术包含 和 程序精化是将 相结合,研究从抽象的 演出具体的面向计算机的 3.模式是Z语言规格中一个重要的元素,模式是由 组成 Larch方法是软件系统规格的一种 Larch方法的程序规格包括 和与目 标语言相关的 两个部分。 二、利用有限状态机描述“AB协议”。(15分) AB协议包含发送端和接收端两个实体。发送端协议实体从发送方用户获取一个报文, 将序号寄存器值赋给报文,然后向接收端协议实体发出报文,发送方发出报文之后启动超时 时钟,等待认可报文。如果在给定的时间内未收到认可报文,则重发报文;如果收到认可报 文,其序号与发出报文序号相同,则发送端实体从发送方用户获取下个报文。接收端协议实 体在收到报文之后,如果报文无错误,则想发送端实体发送认可报文,然后将报文递交给接 收方用户:如果接收的报文有错误或者序号不正确,则丢失报文。假定所用通道不会中断 报文重复n次后最终能够被接收;认可报文只要发出就能正确收到:报文不会损坏;序号寄 存器初始化为0 三、构造下图所示 Petri网的覆盖树。(10分)
---------------------------------------------------------------------------- （3） ---------ChangeEntry---------------- ∆PhoneDB name?: Person newnumber?: Phone --------------------------------------------- name? ∈dom hasphone hasphone’=( {name?} hasphone)∪{name? newnumber?} ---------------------------------------------------------------------------- 模拟试题三 《软件形式化方法》期末考试试题 （120 分钟） 题号 一 二 三 四 五 六 七 总分 题分 得分 一、填空题。（20 分） 1. 软件危机是指在计算机软件的 过程中所遇到的一系列严重的问题，应对软件危机 的方式分为两种方法： 和 。对于软件开发组织和管理的规范化方法中，主要研 究 、 和 三个要素。 2. 形式化方法研究如何把（具有清晰数学基础的） （描述形式、技术和过程等） 融入软件开发的各个阶段；包括 、形式化验证和程序精化三种活动。形式化验证主 要技术包含 和 ；程序精化是将 与 相结合，研究从抽象的 推 演出具体的面向计算机的 。 3. 模式是 Z 语言规格中一个重要的元素，模式是由 、 和 组成。 4. Larch 方法是软件系统规格的一种 ；Larch 方法的程序规格包括 和与目 标语言相关的 两个部分。 二、利用有限状态机描述“AB 协议”。（15 分） AB 协议包含发送端和接收端两个实体。发送端协议实体从发送方用户获取一个报文， 将序号寄存器值赋给报文，然后向接收端协议实体发出报文，发送方发出报文之后启动超时 时钟，等待认可报文。如果在给定的时间内未收到认可报文，则重发报文；如果收到认可报 文，其序号与发出报文序号相同，则发送端实体从发送方用户获取下个报文。接收端协议实 体在收到报文之后，如果报文无错误，则想发送端实体发送认可报文，然后将报文递交给接 收方用户；如果接收的报文有错误或者序号不正确，则丢失报文。假定所用通道不会中断； 报文重复 n 次后最终能够被接收；认可报文只要发出就能正确收到；报文不会损坏；序号寄 存器初始化为 0 。 三、构造下图所示 Petri 网的覆盖树。（10 分）
四、利用CSP对“生产者消费者”系统进行规格。(10分) 五、逻辑演算证明。(15分) (1)-(QVR)∧(P→Q)P (2)(P→(Q→S)∧(RVP)∧Q卜R→S (3)(3x)P(x)→(Vx)P(x)vQx)→R(x),(3x)P(x)(3x)Q(x)卜R(a)AR(c) 、如图中所示的 Kripke结构,利用标号算法对公式进行模型检验。(15) (1)E(p∧r)>p) (2)A(p>q)=-E(_(pDq) 七、对于哲学家就餐问题,利用CTL描述下述性质。(15) (1)相邻的两个哲学家不能同时都在用餐 (2)一个哲学家只要处于等待用餐状态,就可以最终进入用餐状态 (3)存在一个状态使得该状态下每个哲学家都拿起一把叉子
四、利用 CSP 对“生产者-消费者”系统进行规格。（10 分） 五、逻辑演算证明。（15 分） （1）(Q∨R) ∧(P→Q)├P （2）(P→(Q→S)) ∧ (R∨P) ∧Q├ R→S （3）(x)P(x)→(x)(P(x)Q(x)→R(x)), (x)P(x), (x)Q(x)├ R(a)R(c) 六、如图中所示的 Kripke 结构，利用标号算法对公式进行模型检验。（15） （1）E((p ∧r) ▷p) （2）A(p▷q) = E((p▷q)) 七、对于哲学家就餐问题，利用 CTL 描述下述性质。（15） （1）相邻的两个哲学家不能同时都在用餐； （2）一个哲学家只要处于等待用餐状态，就可以最终进入用餐状态； （3）存在一个状态使得该状态下每个哲学家都拿起一把叉子