1 Deterministic Automata 1 Deterministic Automata
2 ====================== 2 ======================
3 3
4 Formally, a deterministic automaton, denoted b 4 Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
5 5
6 *G* = { *X*, *E*, *f*, x\ :subscript:` 6 *G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
7 7
8 where: 8 where:
9 9
10 - *X* is the set of states; 10 - *X* is the set of states;
11 - *E* is the finite set of events; 11 - *E* is the finite set of events;
12 - x\ :subscript:`0` is the initial state; 12 - x\ :subscript:`0` is the initial state;
13 - X\ :subscript:`m` (subset of *X*) is the set 13 - X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
14 - *f* : *X* x *E* -> *X* $ is the transition f 14 - *f* : *X* x *E* -> *X* $ is the transition function. It defines the state
15 transition in the occurrence of an event fro 15 transition in the occurrence of an event from *E* in the state *X*. In the
16 special case of deterministic automata, the 16 special case of deterministic automata, the occurrence of the event in *E*
17 in a state in *X* has a deterministic next s 17 in a state in *X* has a deterministic next state from *X*.
18 18
19 For example, a given automaton named 'wip' (wa 19 For example, a given automaton named 'wip' (wakeup in preemptive) can
20 be defined as: 20 be defined as:
21 21
22 - *X* = { ``preemptive``, ``non_preemptive``} 22 - *X* = { ``preemptive``, ``non_preemptive``}
23 - *E* = { ``preempt_enable``, ``preempt_disabl 23 - *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
24 - x\ :subscript:`0` = ``preemptive`` 24 - x\ :subscript:`0` = ``preemptive``
25 - X\ :subscript:`m` = {``preemptive``} 25 - X\ :subscript:`m` = {``preemptive``}
26 - *f* = 26 - *f* =
27 - *f*\ (``preemptive``, ``preempt_disable`` 27 - *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
28 - *f*\ (``non_preemptive``, ``sched_waking` 28 - *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
29 - *f*\ (``non_preemptive``, ``preempt_enabl 29 - *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
30 30
31 One of the benefits of this formal definition 31 One of the benefits of this formal definition is that it can be presented
32 in multiple formats. For example, using a *gra 32 in multiple formats. For example, using a *graphical representation*, using
33 vertices (nodes) and edges, which is very intu 33 vertices (nodes) and edges, which is very intuitive for *operating system*
34 practitioners, without any loss. 34 practitioners, without any loss.
35 35
36 The previous 'wip' automaton can also be repre 36 The previous 'wip' automaton can also be represented as::
37 37
38 preempt_enable 38 preempt_enable
39 +---------------------------------+ 39 +---------------------------------+
40 v | 40 v |
41 #============# preempt_disable +--- 41 #============# preempt_disable +------------------+
42 --> H preemptive H -----------------> | n 42 --> H preemptive H -----------------> | non_preemptive |
43 #============# +--- 43 #============# +------------------+
44 ^ 44 ^ |
45 | 45 | sched_waking |
46 +- 46 +--------------+
47 47
48 Deterministic Automaton in C 48 Deterministic Automaton in C
49 ---------------------------- 49 ----------------------------
50 50
51 In the paper "Efficient formal verification fo 51 In the paper "Efficient formal verification for the Linux kernel",
52 the authors present a simple way to represent 52 the authors present a simple way to represent an automaton in C that can
53 be used as regular code in the Linux kernel. 53 be used as regular code in the Linux kernel.
54 54
55 For example, the 'wip' automata can be present 55 For example, the 'wip' automata can be presented as (augmented with comments)::
56 56
57 /* enum representation of X (set of states) 57 /* enum representation of X (set of states) to be used as index */
58 enum states { 58 enum states {
59 preemptive = 0, 59 preemptive = 0,
60 non_preemptive, 60 non_preemptive,
61 state_max 61 state_max
62 }; 62 };
63 63
64 #define INVALID_STATE state_max 64 #define INVALID_STATE state_max
65 65
66 /* enum representation of E (set of events) 66 /* enum representation of E (set of events) to be used as index */
67 enum events { 67 enum events {
68 preempt_disable = 0, 68 preempt_disable = 0,
69 preempt_enable, 69 preempt_enable,
70 sched_waking, 70 sched_waking,
71 event_max 71 event_max
72 }; 72 };
73 73
74 struct automaton { 74 struct automaton {
75 char *state_names[state_max]; 75 char *state_names[state_max]; // X: the set of states
76 char *event_names[event_max]; 76 char *event_names[event_max]; // E: the finite set of events
77 unsigned char function[state_max][even 77 unsigned char function[state_max][event_max]; // f: transition function
78 unsigned char initial_state; 78 unsigned char initial_state; // x_0: the initial state
79 bool final_states[state_max]; 79 bool final_states[state_max]; // X_m: the set of marked states
80 }; 80 };
81 81
82 struct automaton aut = { 82 struct automaton aut = {
83 .state_names = { 83 .state_names = {
84 "preemptive", 84 "preemptive",
85 "non_preemptive" 85 "non_preemptive"
86 }, 86 },
87 .event_names = { 87 .event_names = {
88 "preempt_disable", 88 "preempt_disable",
89 "preempt_enable", 89 "preempt_enable",
90 "sched_waking" 90 "sched_waking"
91 }, 91 },
92 .function = { 92 .function = {
93 { non_preemptive, INVALID_STA 93 { non_preemptive, INVALID_STATE, INVALID_STATE },
94 { INVALID_STATE, preempti 94 { INVALID_STATE, preemptive, non_preemptive },
95 }, 95 },
96 .initial_state = preemptive, 96 .initial_state = preemptive,
97 .final_states = { 1, 0 }, 97 .final_states = { 1, 0 },
98 }; 98 };
99 99
100 The *transition function* is represented as a 100 The *transition function* is represented as a matrix of states (lines) and
101 events (columns), and so the function *f* : *X 101 events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
102 in O(1). For example:: 102 in O(1). For example::
103 103
104 next_state = automaton_wip.function[curr_sta 104 next_state = automaton_wip.function[curr_state][event];
105 105
106 Graphviz .dot format 106 Graphviz .dot format
107 -------------------- 107 --------------------
108 108
109 The Graphviz open-source tool can produce the 109 The Graphviz open-source tool can produce the graphical representation
110 of an automaton using the (textual) DOT langua 110 of an automaton using the (textual) DOT language as the source code.
111 The DOT format is widely used and can be conve 111 The DOT format is widely used and can be converted to many other formats.
112 112
113 For example, this is the 'wip' model in DOT:: 113 For example, this is the 'wip' model in DOT::
114 114
115 digraph state_automaton { 115 digraph state_automaton {
116 {node [shape = circle] "non_preemptive 116 {node [shape = circle] "non_preemptive"};
117 {node [shape = plaintext, style=invis, 117 {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
118 {node [shape = doublecircle] "preempti 118 {node [shape = doublecircle] "preemptive"};
119 {node [shape = circle] "preemptive"}; 119 {node [shape = circle] "preemptive"};
120 "__init_preemptive" -> "preemptive"; 120 "__init_preemptive" -> "preemptive";
121 "non_preemptive" [label = "non_preempt 121 "non_preemptive" [label = "non_preemptive"];
122 "non_preemptive" -> "non_preemptive" [ 122 "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
123 "non_preemptive" -> "preemptive" [ lab 123 "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
124 "preemptive" [label = "preemptive"]; 124 "preemptive" [label = "preemptive"];
125 "preemptive" -> "non_preemptive" [ lab 125 "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
126 { rank = min ; 126 { rank = min ;
127 "__init_preemptive"; 127 "__init_preemptive";
128 "preemptive"; 128 "preemptive";
129 } 129 }
130 } 130 }
131 131
132 This DOT format can be transformed into a bitm 132 This DOT format can be transformed into a bitmap or vectorial image
133 using the dot utility, or into an ASCII art us 133 using the dot utility, or into an ASCII art using graph-easy. For
134 instance:: 134 instance::
135 135
136 $ dot -Tsvg -o wip.svg wip.dot 136 $ dot -Tsvg -o wip.svg wip.dot
137 $ graph-easy wip.dot > wip.txt 137 $ graph-easy wip.dot > wip.txt
138 138
139 dot2c 139 dot2c
140 ----- 140 -----
141 141
142 dot2c is a utility that can parse a .dot file 142 dot2c is a utility that can parse a .dot file containing an automaton as
143 in the example above and automatically convert 143 in the example above and automatically convert it to the C representation
144 presented in [3]. 144 presented in [3].
145 145
146 For example, having the previous 'wip' model i 146 For example, having the previous 'wip' model into a file named 'wip.dot',
147 the following command will transform the .dot 147 the following command will transform the .dot file into the C
148 representation (previously shown) in the 'wip. 148 representation (previously shown) in the 'wip.h' file::
149 149
150 $ dot2c wip.dot > wip.h 150 $ dot2c wip.dot > wip.h
151 151
152 The 'wip.h' content is the code sample in sect 152 The 'wip.h' content is the code sample in section 'Deterministic Automaton
153 in C'. 153 in C'.
154 154
155 Remarks 155 Remarks
156 ------- 156 -------
157 157
158 The automata formalism allows modeling discret 158 The automata formalism allows modeling discrete event systems (DES) in
159 multiple formats, suitable for different appli 159 multiple formats, suitable for different applications/users.
160 160
161 For example, the formal description using set 161 For example, the formal description using set theory is better suitable
162 for automata operations, while the graphical f 162 for automata operations, while the graphical format for human interpretation;
163 and computer languages for machine execution. 163 and computer languages for machine execution.
164 164
165 References 165 References
166 ---------- 166 ----------
167 167
168 Many textbooks cover automata formalism. For a 168 Many textbooks cover automata formalism. For a brief introduction see::
169 169
170 O'Regan, Gerard. Concise guide to software e 170 O'Regan, Gerard. Concise guide to software engineering. Springer,
171 Cham, 2017. 171 Cham, 2017.
172 172
173 For a detailed description, including operatio 173 For a detailed description, including operations, and application on Discrete
174 Event Systems (DES), see:: 174 Event Systems (DES), see::
175 175
176 Cassandras, Christos G., and Stephane Lafort 176 Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
177 event systems. Boston, MA: Springer US, 2008 177 event systems. Boston, MA: Springer US, 2008.
178 178
179 For the C representation in kernel, see:: 179 For the C representation in kernel, see::
180 180
181 De Oliveira, Daniel Bristot; Cucinotta, Tomm 181 De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
182 Silva. Efficient formal verification for the 182 Silva. Efficient formal verification for the Linux kernel. In:
183 International Conference on Software Enginee 183 International Conference on Software Engineering and Formal Methods.
184 Springer, Cham, 2019. p. 315-332. 184 Springer, Cham, 2019. p. 315-332.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.