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

一、概述

1.1 软件工程方法分类

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

1.2 非形式化方法的缺点

1.3 形式化方法的优点

1.4 应用形式化方法的准则

二、有穷状态机

2.1 保险箱状态转换图

#mermaid-svg-aL2VrfEb0PopXUpc .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-aL2VrfEb0PopXUpc .label text{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .node rect,#mermaid-svg-aL2VrfEb0PopXUpc .node circle,#mermaid-svg-aL2VrfEb0PopXUpc .node ellipse,#mermaid-svg-aL2VrfEb0PopXUpc .node polygon,#mermaid-svg-aL2VrfEb0PopXUpc .node path{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-aL2VrfEb0PopXUpc .node .label{text-align:center;fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .node.clickable{cursor:pointer}#mermaid-svg-aL2VrfEb0PopXUpc .arrowheadPath{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .edgePath .path{stroke:#333;stroke-width:1.5px}#mermaid-svg-aL2VrfEb0PopXUpc .flowchart-link{stroke:#333;fill:none}#mermaid-svg-aL2VrfEb0PopXUpc .edgeLabel{background-color:#e8e8e8;text-align:center}#mermaid-svg-aL2VrfEb0PopXUpc .edgeLabel rect{opacity:0.9}#mermaid-svg-aL2VrfEb0PopXUpc .edgeLabel span{color:#333}#mermaid-svg-aL2VrfEb0PopXUpc .cluster rect{fill:#ffffde;stroke:#aa3;stroke-width:1px}#mermaid-svg-aL2VrfEb0PopXUpc .cluster text{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:12px;background:#ffffde;border:1px solid #aa3;border-radius:2px;pointer-events:none;z-index:100}#mermaid-svg-aL2VrfEb0PopXUpc .actor{stroke:#ccf;fill:#ECECFF}#mermaid-svg-aL2VrfEb0PopXUpc text.actor>tspan{fill:#000;stroke:none}#mermaid-svg-aL2VrfEb0PopXUpc .actor-line{stroke:grey}#mermaid-svg-aL2VrfEb0PopXUpc .messageLine0{stroke-width:1.5;stroke-dasharray:none;stroke:#333}#mermaid-svg-aL2VrfEb0PopXUpc .messageLine1{stroke-width:1.5;stroke-dasharray:2, 2;stroke:#333}#mermaid-svg-aL2VrfEb0PopXUpc #arrowhead path{fill:#333;stroke:#333}#mermaid-svg-aL2VrfEb0PopXUpc .sequenceNumber{fill:#fff}#mermaid-svg-aL2VrfEb0PopXUpc #sequencenumber{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc #crosshead path{fill:#333;stroke:#333}#mermaid-svg-aL2VrfEb0PopXUpc .messageText{fill:#333;stroke:#333}#mermaid-svg-aL2VrfEb0PopXUpc .labelBox{stroke:#ccf;fill:#ECECFF}#mermaid-svg-aL2VrfEb0PopXUpc .labelText,#mermaid-svg-aL2VrfEb0PopXUpc .labelText>tspan{fill:#000;stroke:none}#mermaid-svg-aL2VrfEb0PopXUpc .loopText,#mermaid-svg-aL2VrfEb0PopXUpc .loopText>tspan{fill:#000;stroke:none}#mermaid-svg-aL2VrfEb0PopXUpc .loopLine{stroke-width:2px;stroke-dasharray:2, 2;stroke:#ccf;fill:#ccf}#mermaid-svg-aL2VrfEb0PopXUpc .note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-aL2VrfEb0PopXUpc .noteText,#mermaid-svg-aL2VrfEb0PopXUpc .noteText>tspan{fill:#000;stroke:none}#mermaid-svg-aL2VrfEb0PopXUpc .activation0{fill:#f4f4f4;stroke:#666}#mermaid-svg-aL2VrfEb0PopXUpc .activation1{fill:#f4f4f4;stroke:#666}#mermaid-svg-aL2VrfEb0PopXUpc .activation2{fill:#f4f4f4;stroke:#666}#mermaid-svg-aL2VrfEb0PopXUpc .mermaid-main-font{font-family:"trebuchet ms", verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .section{stroke:none;opacity:0.2}#mermaid-svg-aL2VrfEb0PopXUpc .section0{fill:rgba(102,102,255,0.49)}#mermaid-svg-aL2VrfEb0PopXUpc .section2{fill:#fff400}#mermaid-svg-aL2VrfEb0PopXUpc .section1,#mermaid-svg-aL2VrfEb0PopXUpc .section3{fill:#fff;opacity:0.2}#mermaid-svg-aL2VrfEb0PopXUpc .sectionTitle0{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .sectionTitle1{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .sectionTitle2{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .sectionTitle3{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .sectionTitle{text-anchor:start;font-size:11px;text-height:14px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .grid .tick{stroke:#d3d3d3;opacity:0.8;shape-rendering:crispEdges}#mermaid-svg-aL2VrfEb0PopXUpc .grid .tick text{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .grid path{stroke-width:0}#mermaid-svg-aL2VrfEb0PopXUpc .today{fill:none;stroke:red;stroke-width:2px}#mermaid-svg-aL2VrfEb0PopXUpc .task{stroke-width:2}#mermaid-svg-aL2VrfEb0PopXUpc .taskText{text-anchor:middle;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .taskText:not([font-size]){font-size:11px}#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutsideRight{fill:#000;text-anchor:start;font-size:11px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutsideLeft{fill:#000;text-anchor:end;font-size:11px}#mermaid-svg-aL2VrfEb0PopXUpc .task.clickable{cursor:pointer}#mermaid-svg-aL2VrfEb0PopXUpc .taskText.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutsideLeft.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutsideRight.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-aL2VrfEb0PopXUpc .taskText0,#mermaid-svg-aL2VrfEb0PopXUpc .taskText1,#mermaid-svg-aL2VrfEb0PopXUpc .taskText2,#mermaid-svg-aL2VrfEb0PopXUpc .taskText3{fill:#fff}#mermaid-svg-aL2VrfEb0PopXUpc .task0,#mermaid-svg-aL2VrfEb0PopXUpc .task1,#mermaid-svg-aL2VrfEb0PopXUpc .task2,#mermaid-svg-aL2VrfEb0PopXUpc .task3{fill:#8a90dd;stroke:#534fbc}#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutside0,#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutside2{fill:#000}#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutside1,#mermaid-svg-aL2VrfEb0PopXUpc .taskTextOutside3{fill:#000}#mermaid-svg-aL2VrfEb0PopXUpc .active0,#mermaid-svg-aL2VrfEb0PopXUpc .active1,#mermaid-svg-aL2VrfEb0PopXUpc .active2,#mermaid-svg-aL2VrfEb0PopXUpc .active3{fill:#bfc7ff;stroke:#534fbc}#mermaid-svg-aL2VrfEb0PopXUpc .activeText0,#mermaid-svg-aL2VrfEb0PopXUpc .activeText1,#mermaid-svg-aL2VrfEb0PopXUpc .activeText2,#mermaid-svg-aL2VrfEb0PopXUpc .activeText3{fill:#000 !important}#mermaid-svg-aL2VrfEb0PopXUpc .done0,#mermaid-svg-aL2VrfEb0PopXUpc .done1,#mermaid-svg-aL2VrfEb0PopXUpc .done2,#mermaid-svg-aL2VrfEb0PopXUpc .done3{stroke:grey;fill:#d3d3d3;stroke-width:2}#mermaid-svg-aL2VrfEb0PopXUpc .doneText0,#mermaid-svg-aL2VrfEb0PopXUpc .doneText1,#mermaid-svg-aL2VrfEb0PopXUpc .doneText2,#mermaid-svg-aL2VrfEb0PopXUpc .doneText3{fill:#000 !important}#mermaid-svg-aL2VrfEb0PopXUpc .crit0,#mermaid-svg-aL2VrfEb0PopXUpc .crit1,#mermaid-svg-aL2VrfEb0PopXUpc .crit2,#mermaid-svg-aL2VrfEb0PopXUpc .crit3{stroke:#f88;fill:red;stroke-width:2}#mermaid-svg-aL2VrfEb0PopXUpc .activeCrit0,#mermaid-svg-aL2VrfEb0PopXUpc .activeCrit1,#mermaid-svg-aL2VrfEb0PopXUpc .activeCrit2,#mermaid-svg-aL2VrfEb0PopXUpc .activeCrit3{stroke:#f88;fill:#bfc7ff;stroke-width:2}#mermaid-svg-aL2VrfEb0PopXUpc .doneCrit0,#mermaid-svg-aL2VrfEb0PopXUpc .doneCrit1,#mermaid-svg-aL2VrfEb0PopXUpc .doneCrit2,#mermaid-svg-aL2VrfEb0PopXUpc .doneCrit3{stroke:#f88;fill:#d3d3d3;stroke-width:2;cursor:pointer;shape-rendering:crispEdges}#mermaid-svg-aL2VrfEb0PopXUpc .milestone{transform:rotate(45deg) scale(0.8, 0.8)}#mermaid-svg-aL2VrfEb0PopXUpc .milestoneText{font-style:italic}#mermaid-svg-aL2VrfEb0PopXUpc .doneCritText0,#mermaid-svg-aL2VrfEb0PopXUpc .doneCritText1,#mermaid-svg-aL2VrfEb0PopXUpc .doneCritText2,#mermaid-svg-aL2VrfEb0PopXUpc .doneCritText3{fill:#000 !important}#mermaid-svg-aL2VrfEb0PopXUpc .activeCritText0,#mermaid-svg-aL2VrfEb0PopXUpc .activeCritText1,#mermaid-svg-aL2VrfEb0PopXUpc .activeCritText2,#mermaid-svg-aL2VrfEb0PopXUpc .activeCritText3{fill:#000 !important}#mermaid-svg-aL2VrfEb0PopXUpc .titleText{text-anchor:middle;font-size:18px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc g.classGroup text{fill:#9370db;stroke:none;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:10px}#mermaid-svg-aL2VrfEb0PopXUpc g.classGroup text .title{font-weight:bolder}#mermaid-svg-aL2VrfEb0PopXUpc g.clickable{cursor:pointer}#mermaid-svg-aL2VrfEb0PopXUpc g.classGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-aL2VrfEb0PopXUpc g.classGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc .classLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.5}#mermaid-svg-aL2VrfEb0PopXUpc .classLabel .label{fill:#9370db;font-size:10px}#mermaid-svg-aL2VrfEb0PopXUpc .relation{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-aL2VrfEb0PopXUpc .dashed-line{stroke-dasharray:3}#mermaid-svg-aL2VrfEb0PopXUpc #compositionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc #compositionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc #aggregationStart{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc #aggregationEnd{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc #dependencyStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc #dependencyEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc #extensionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc #extensionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc .commit-id,#mermaid-svg-aL2VrfEb0PopXUpc .commit-msg,#mermaid-svg-aL2VrfEb0PopXUpc .branch-label{fill:lightgrey;color:lightgrey;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .pieTitleText{text-anchor:middle;font-size:25px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .slice{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc g.stateGroup text{fill:#9370db;stroke:none;font-size:10px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc g.stateGroup text{fill:#9370db;fill:#333;stroke:none;font-size:10px}#mermaid-svg-aL2VrfEb0PopXUpc g.statediagram-cluster .cluster-label text{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc g.stateGroup .state-title{font-weight:bolder;fill:#000}#mermaid-svg-aL2VrfEb0PopXUpc g.stateGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-aL2VrfEb0PopXUpc g.stateGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-aL2VrfEb0PopXUpc .transition{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-aL2VrfEb0PopXUpc .stateGroup .composit{fill:white;border-bottom:1px}#mermaid-svg-aL2VrfEb0PopXUpc .stateGroup .alt-composit{fill:#e0e0e0;border-bottom:1px}#mermaid-svg-aL2VrfEb0PopXUpc .state-note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-aL2VrfEb0PopXUpc .state-note text{fill:black;stroke:none;font-size:10px}#mermaid-svg-aL2VrfEb0PopXUpc .stateLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.7}#mermaid-svg-aL2VrfEb0PopXUpc .edgeLabel text{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .stateLabel text{fill:#000;font-size:10px;font-weight:bold;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-aL2VrfEb0PopXUpc .node circle.state-start{fill:black;stroke:black}#mermaid-svg-aL2VrfEb0PopXUpc .node circle.state-end{fill:black;stroke:white;stroke-width:1.5}#mermaid-svg-aL2VrfEb0PopXUpc #statediagram-barbEnd{fill:#9370db}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-cluster rect{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-cluster rect.outer{rx:5px;ry:5px}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-state .divider{stroke:#9370db}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-state .title-state{rx:5px;ry:5px}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-cluster.statediagram-cluster .inner{fill:white}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-cluster.statediagram-cluster-alt .inner{fill:#e0e0e0}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-cluster .inner{rx:0;ry:0}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-state rect.basic{rx:5px;ry:5px}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-state rect.divider{stroke-dasharray:10,10;fill:#efefef}#mermaid-svg-aL2VrfEb0PopXUpc .note-edge{stroke-dasharray:5}#mermaid-svg-aL2VrfEb0PopXUpc .statediagram-note rect{fill:#fff5ad;stroke:#aa3;stroke-width:1px;rx:0;ry:0}:root{--mermaid-font-family: '"trebuchet ms", verdana, arial';--mermaid-font-family: "Comic Sans MS", "Comic Sans", cursive}#mermaid-svg-aL2VrfEb0PopXUpc .error-icon{fill:#522}#mermaid-svg-aL2VrfEb0PopXUpc .error-text{fill:#522;stroke:#522}#mermaid-svg-aL2VrfEb0PopXUpc .edge-thickness-normal{stroke-width:2px}#mermaid-svg-aL2VrfEb0PopXUpc .edge-thickness-thick{stroke-width:3.5px}#mermaid-svg-aL2VrfEb0PopXUpc .edge-pattern-solid{stroke-dasharray:0}#mermaid-svg-aL2VrfEb0PopXUpc .edge-pattern-dashed{stroke-dasharray:3}#mermaid-svg-aL2VrfEb0PopXUpc .edge-pattern-dotted{stroke-dasharray:2}#mermaid-svg-aL2VrfEb0PopXUpc .marker{fill:#333}#mermaid-svg-aL2VrfEb0PopXUpc .marker.cross{stroke:#333}:root { --mermaid-font-family: "trebuchet ms", verdana, arial;}#mermaid-svg-aL2VrfEb0PopXUpc {color: rgba(0, 0, 0, 0.75);font: ;}

转盘其他移动

保险箱锁定

保险箱解锁

报警

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

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

转换函数T。

初始态S: 保险箱锁定。

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

2.2 转换规则

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

Reference

《软件工程导论》