確定性自動機¶
形式上，一個確定性自動機，記作 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.