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