形式化说明技术有穷状态机

一、概述

1.1 软件工程方法分类

按照形式化的程度进行划分。

1.3 形式化方法的优点

二、有穷状态机

2.1 保险箱状态转换图

1L 3R 2L 转盘其他移动 转盘其他移动 转盘其他移动 保险箱锁定 A B 保险箱解锁 警

状态集J: {保险箱锁定，A，B，保险箱解锁， 警}。

输入集K: {1L，1R，2L，2R，3L，3R}。

转换函数T。

初始态S: 保险箱锁定。

终态集F: {保险箱解锁， 警}。

2.2 转换规则

对一个系统进行规格说明，通常都需要对有穷状态机进行一个扩展，因此需要在前述5个元组中加入第6个部件——谓词集P，其中每个谓词都是系统全局状态Y的函数。则转换规则形式如下：
$$当前状态[菜单]+事件[所选择的项]+谓词=>下个状态$$

Reference

《软件工程导论》