软件形式化方法-西电模拟题-2

学习中心

姓 名学 号

西安电子科技大学网络教育学院

模拟试题二

《软件形式化方法》期末考试试题

（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）E p （3）A(p q)

http:///DOWN/course/rjxshff/mnst/mnst2.htm1/4

软件形式化方法-西电模拟题-2

七、在教材7.3节中描述的电话号码系统中增加下列操作，给出完整的操作模式。（15） （1）收回电话（RemoveEntry）：收回已经分配给某人的电话； （2）查询电话用户（FindNames）：查询指定号码的电话用户； （3）更改电话号码（ChangeEntry）：更改某个用户的电话号码。

参考答案与答题要点

一、填空题

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及前提引入规则

http:///DOWN/course/rjxshff/mnst/mnst2.htm

2/4

软件形式化方法-西电模拟题-2

http:///DOWN/course/rjxshff/mnst/mnst2.htm

5. P∧Q 假设前提引入6. Q 5及基本蕴含公式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={<s0,s1>, <s0,s2>, <s1,s0>, <s1,s3>, <s2,s1>, <s3,s3>} {p,q}， L(s2)={p,r}，L(s3)={q}

A○p：s0, s2成立 s1, s3不成立E p：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）

---------ChangeEntry---------------- PhoneDBn …… 此处隐藏：993字，全部文档内容请下载后查看。喜欢就下载吧 ……