确定性自动机¶
形式上，一个确定性自动机，记作 G，被定义为一个五元组
G = { X, E, f, x0, Xm }
其中
X 是状态集；
E 是事件的有限集；
x0 是初始状态；
Xm（X 的子集）是标记（或最终）状态集。
f : X x E -> X $ 是转移函数。它定义了在状态 X 中发生 E 中的事件时的状态转移。在确定性自动机的特殊情况下，在 X 中的某个状态发生 E 中的事件会有一个确定的下一个状态（来自 X）。
例如，一个名为“wip”（抢占唤醒）的给定自动机可以定义为
X = {
preemptive,non_preemptive}E = {
preempt_enable,preempt_disable,sched_waking}x0 =
preemptiveXm = {
preemptive}- f =
f(
preemptive,preempt_disable) =non_preemptivef(
non_preemptive,sched_waking) =non_preemptivef(
non_preemptive,preempt_enable) =preemptive
这种形式化定义的好处之一是它可以以多种格式呈现。例如，使用图形表示，使用顶点（节点）和边，这对于操作系统从业者来说非常直观，且没有任何损失。
先前的“wip”自动机也可以表示为
preempt_enable
+---------------------------------+
v |
#============# preempt_disable +------------------+
--> H preemptive H -----------------> | non_preemptive |
#============# +------------------+
^ |
| sched_waking |
+--------------+
C 语言中的确定性自动机¶
在论文“Efficient formal verification for the Linux kernel”中，作者提出了一种在 C 语言中表示自动机的简单方法，可以作为常规代码用于 Linux 内核。
例如，“wip”自动机可以表示为（附带注释）
/* enum representation of X (set of states) to be used as index */
enum states {
preemptive = 0,
non_preemptive,
state_max
};
#define INVALID_STATE state_max
/* enum representation of E (set of events) to be used as index */
enum events {
preempt_disable = 0,
preempt_enable,
sched_waking,
event_max
};
struct automaton {
char *state_names[state_max]; // X: the set of states
char *event_names[event_max]; // E: the finite set of events
unsigned char function[state_max][event_max]; // f: transition function
unsigned char initial_state; // x_0: the initial state
bool final_states[state_max]; // X_m: the set of marked states
};
struct automaton aut = {
.state_names = {
"preemptive",
"non_preemptive"
},
.event_names = {
"preempt_disable",
"preempt_enable",
"sched_waking"
},
.function = {
{ non_preemptive, INVALID_STATE, INVALID_STATE },
{ INVALID_STATE, preemptive, non_preemptive },
},
.initial_state = preemptive,
.final_states = { 1, 0 },
};
转移函数表示为状态（行）和事件（列）的矩阵，因此函数 f : X x E -> X 可以在 O(1) 时间内求解。例如
next_state = automaton_wip.function[curr_state][event];
Graphviz .dot 格式¶
Graphviz 开源工具可以使用 (文本) DOT 语言作为源代码生成自动机的图形表示。DOT 格式被广泛使用，并可以转换为许多其他格式。
例如，这是 DOT 格式的“wip”模型
digraph state_automaton {
{node [shape = circle] "non_preemptive"};
{node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
{node [shape = doublecircle] "preemptive"};
{node [shape = circle] "preemptive"};
"__init_preemptive" -> "preemptive";
"non_preemptive" [label = "non_preemptive"];
"non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
"non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
"preemptive" [label = "preemptive"];
"preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
{ rank = min ;
"__init_preemptive";
"preemptive";
}
}
这种 DOT 格式可以使用 dot 工具转换为位图或矢量图像，或者使用 graph-easy 转换为 ASCII 艺术。例如
$ dot -Tsvg -o wip.svg wip.dot
$ graph-easy wip.dot > wip.txt
dot2c¶
dot2c 是一个工具，它可以解析包含如上例所示自动机的 .dot 文件，并自动将其转换为 [3] 中介绍的 C 语言表示。
例如，将先前的“wip”模型保存到名为“wip.dot”的文件中，以下命令将把 .dot 文件转换为“wip.h”文件中的 C 语言表示（如前所示）
$ dot2c wip.dot > wip.h
“wip.h”的内容是“C 语言中的确定性自动机”一节中的代码示例。
备注¶
自动机形式化允许以多种格式对离散事件系统 (DES) 进行建模，适用于不同的应用/用户。
例如，使用集合论的形式描述更适合自动机操作，而图形格式适合人类解释；计算机语言则适合机器执行。
参考文献¶
许多教科书都涵盖自动机形式化。简要介绍请参见
O'Regan, Gerard. Concise guide to software engineering. Springer,
Cham, 2017.
有关详细描述，包括操作和在离散事件系统 (DES) 上的应用，请参见
Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
event systems. Boston, MA: Springer US, 2008.
有关内核中的 C 语言表示，请参见
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
Silva. Efficient formal verification for the Linux kernel. In:
International Conference on Software Engineering and Formal Methods.
Springer, Cham, 2019. p. 315-332.