学习中心
姓名学号
西安电子科技大学网络教育
2012学年上学期
《软件形式化方法》期末考试试题
（综合大作业）
考试说明：
1．大作业于2012年06月09日下发，2012年06月23日交回。

2．试题必须独立完成，如发现抄袭、雷同均按零分计。

3．试题须手写完成，卷面字迹工整，不能提交打印稿。

一填空题（每空2分，合计30分）
1. 现代软件工程的软件定义包括、和。

2. 软件危机是指在计算机软件的开发和维护过程中所遇到的一系列严重的问题，其产生的原因主要包括：、、、；其本质特征是软件的和。

3. 模式是Z语言规格中一个重要的元素，模式是由、和
组成。

4. 形式化方法研究如何把（具有清晰数学基础的）严格性（描述形式、技术和过程等）融入软件开发的各个阶段；包括形式化规格、和三种活动，在软件开发的形式化规格中包含的三种规格为、和。

二有限状态机（10分）
对于图中所示有限状态机的状态转移图，给出其关系矩阵和状态转移表。

三Petri网（10分）
对图中所示Petri网进行化简。

四进程代数（10分）
（1）计算进程PHONE的迹
PHONE = ring → answer → hungup→ STOP
（2）给出迹投影结果
<start, ask, answer, wrong, start, ask, answer, right, end>↑{start, ask, end}五命题和逻辑演算（每题10分合计20分）
（1）P∧(Q↔R)├(P∧Q) ↔(P∧R)
（2）├ (∃x)(P(X) →(∀Y)P(Y))
六时态逻辑（每题10分合计20分）
对于图中所示的Kripke结构，利用标号算法对公式进行模型检验。

（1）E((p ∧r)▷p)
（2）A(p▷q) = ⌝E(⌝(p▷q))。