本文用书：《软件工程导论》 第六版 清华大学出版社
1.有穷状态机
2.peri网技术
第四章 形式化说明技术
4.1 概述
1.非形式化方法的缺点
用自然语言书写的系统规格说明书,可能存在矛盾,二义性,含糊性,不完整性及抽象层次混乱等问题。
2.形式化方法的优点
能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具；
可以在不同的软件工程活动之间平滑地过渡；
它提供了高层确认的手段。
3.应用形式化方法的准则
应该选用适当的表示方法。
应该形式化，但不要过分形式化。
应该估算成本。
应该有形式化方法顾问随时提供咨询。
不应该放弃传统的开发方法。 应该建立详尽的文档。
不应该放弃质量标准。
不应该盲目依赖形式化方法。
应该测试、测试再测试。
应该重用。
4.2 有穷状态机
1.概念：
如果使用更形式化的术语，一个有穷状态机可以表示为一个5元组(J，K，T，S，F)，其中：
J是一个有穷的非空状态集；
K是一个有穷的非空输入集；
T是一个从(J-F)×K到J的转换函数；
S∈J，是一个初始状态；
FJ，是终态集。
2.例子
一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。
图4.1描绘了保险箱的状态转换情况。
保险箱的例子，相应的有穷状态机的各部分如下：
状态集J：｛保险箱锁定，A，B，保险箱解锁，报警｝。
输入集K：｛1L，1R，2L，2R，3L，3R｝。
转换函数T：如表4.1所示。
初始态S：保险箱锁定。
终态集F：｛保险箱解锁，报警｝。
4.3 peri网技术
1. 用于确定系统中隐含的定时问题的一种有效技术是Petri网，可以有效地描述并发活动。
2.组成：
一组位置P为｛P1，P2，P3，P4｝，在图中用圆圈代表位置。
一组转换T为｛t1，t2｝，在图中用短直线表示转换。
两个用于转换的输入函数，用由位置指向转换的箭头表示，它们是：I(t1)=｛P2，P4｝；I(t2)=｛P2｝
两个用于转换的输出函数，用由转换指向位置的箭头表示，它们是：O(t1)=｛P1｝；O(t2)=｛P3，P3｝
输出函数O(t2)中有两个P3，是因为有两个箭头由t2指向P3
2.权标
Petri网的标记是在Petri网中权标(token)的分配。
例如，在图4.6中有4个权标，其中一个在P1中，两个在P2中，P3中没有，还有一个在P4中。上述标记可以用向量(1，2，0，1)表示。由于P2和P4中有权标，因此t1启动(即被激发)。 通常，当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。 当t1被激发时，P2和P4上各有一个权标被移出，而P1上则增加一个权标。Petri网中权标总数不是固定的，在这个例子中两个权标被移出，而P1上只能增加一个权标。
在图4.6中P2上有权标，因此t2也可以被激发。当t2被激发时，P2上将移走一个权标，而P3上新增加两个权标。 Petri网具有非确定性，也就是说，如果数个转换都达到了激发条件，则其中任意一个都可以被激发。 图4.6所示Petri网的标记为(1，2，0，1)，t1和t2都可以被激发。假设t1被激发了，则结果如下图4.7所示，标记为(2，1，0，0)。 此时，只有t2可以被激发。如果t2也被激发了，则权标从P2中移出，两个新权标被放在P3上，结果如下图4.8所示，标记为(2，0，2，0)。
4.4 Z语言（略）
