按形式化程度，可以将软件工程使用的方法分为：
用自然语言书写的缺点：矛盾，二义性，含糊性，不完整性 矛盾—一组相互冲突的描述 二义性——读者可以用不同方式进行解读
优点：
一种形式化方法 用图形表示一个例子：
同时也可以用表格表示： 有穷状态机可以表现成一个五元组 （J,K,T,S,F） 1）状态集J：{保险箱锁定，A，B，保险箱解锁，报警} 2）输入集K：{1L,1R,2L,2R,3L,3R} 3）转换函数T，如表4.1 4）初始状态S：保险箱锁定 5）终态集F：{保险箱解锁，报警}
格式： 当前状态+事件+谓词 ——》下个状态
评价：
解决定时问题，尤其是那些有异步和并发活动的系统
当每个输入位置所拥有的权标数>=从该位置到转换的线数时，就允许转换 初始： T1被激发 t2被激发
当输入线上至少有一个输入没有权标的时候才允许转化激发。 EBf有一个权标，表示电梯内楼层f的按钮被按下了 电梯只有第一次按下才会亮，往后再按都没有反应
