0001 Deterministic Automata
0002 ======================
0003
0004 Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
0005
0006 *G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
0007
0008 where:
0009
0010 - *X* is the set of states;
0011 - *E* is the finite set of events;
0012 - x\ :subscript:`0` is the initial state;
0013 - X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
0014 - *f* : *X* x *E* -> *X* $ is the transition function. It defines the state
0015 transition in the occurrence of an event from *E* in the state *X*. In the
0016 special case of deterministic automata, the occurrence of the event in *E*
0017 in a state in *X* has a deterministic next state from *X*.
0018
0019 For example, a given automaton named 'wip' (wakeup in preemptive) can
0020 be defined as:
0021
0022 - *X* = { ``preemptive``, ``non_preemptive``}
0023 - *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
0024 - x\ :subscript:`0` = ``preemptive``
0025 - X\ :subscript:`m` = {``preemptive``}
0026 - *f* =
0027 - *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
0028 - *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
0029 - *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
0030
0031 One of the benefits of this formal definition is that it can be presented
0032 in multiple formats. For example, using a *graphical representation*, using
0033 vertices (nodes) and edges, which is very intuitive for *operating system*
0034 practitioners, without any loss.
0035
0036 The previous 'wip' automaton can also be represented as::
0037
0038 preempt_enable
0039 +---------------------------------+
0040 v |
0041 #============# preempt_disable +------------------+
0042 --> H preemptive H -----------------> | non_preemptive |
0043 #============# +------------------+
0044 ^ |
0045 | sched_waking |
0046 +--------------+
0047
0048 Deterministic Automaton in C
0049 ----------------------------
0050
0051 In the paper "Efficient formal verification for the Linux kernel",
0052 the authors present a simple way to represent an automaton in C that can
0053 be used as regular code in the Linux kernel.
0054
0055 For example, the 'wip' automata can be presented as (augmented with comments)::
0056
0057 /* enum representation of X (set of states) to be used as index */
0058 enum states {
0059 preemptive = 0,
0060 non_preemptive,
0061 state_max
0062 };
0063
0064 #define INVALID_STATE state_max
0065
0066 /* enum representation of E (set of events) to be used as index */
0067 enum events {
0068 preempt_disable = 0,
0069 preempt_enable,
0070 sched_waking,
0071 event_max
0072 };
0073
0074 struct automaton {
0075 char *state_names[state_max]; // X: the set of states
0076 char *event_names[event_max]; // E: the finite set of events
0077 unsigned char function[state_max][event_max]; // f: transition function
0078 unsigned char initial_state; // x_0: the initial state
0079 bool final_states[state_max]; // X_m: the set of marked states
0080 };
0081
0082 struct automaton aut = {
0083 .state_names = {
0084 "preemptive",
0085 "non_preemptive"
0086 },
0087 .event_names = {
0088 "preempt_disable",
0089 "preempt_enable",
0090 "sched_waking"
0091 },
0092 .function = {
0093 { non_preemptive, INVALID_STATE, INVALID_STATE },
0094 { INVALID_STATE, preemptive, non_preemptive },
0095 },
0096 .initial_state = preemptive,
0097 .final_states = { 1, 0 },
0098 };
0099
0100 The *transition function* is represented as a matrix of states (lines) and
0101 events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
0102 in O(1). For example::
0103
0104 next_state = automaton_wip.function[curr_state][event];
0105
0106 Graphviz .dot format
0107 --------------------
0108
0109 The Graphviz open-source tool can produce the graphical representation
0110 of an automaton using the (textual) DOT language as the source code.
0111 The DOT format is widely used and can be converted to many other formats.
0112
0113 For example, this is the 'wip' model in DOT::
0114
0115 digraph state_automaton {
0116 {node [shape = circle] "non_preemptive"};
0117 {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
0118 {node [shape = doublecircle] "preemptive"};
0119 {node [shape = circle] "preemptive"};
0120 "__init_preemptive" -> "preemptive";
0121 "non_preemptive" [label = "non_preemptive"];
0122 "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
0123 "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
0124 "preemptive" [label = "preemptive"];
0125 "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
0126 { rank = min ;
0127 "__init_preemptive";
0128 "preemptive";
0129 }
0130 }
0131
0132 This DOT format can be transformed into a bitmap or vectorial image
0133 using the dot utility, or into an ASCII art using graph-easy. For
0134 instance::
0135
0136 $ dot -Tsvg -o wip.svg wip.dot
0137 $ graph-easy wip.dot > wip.txt
0138
0139 dot2c
0140 -----
0141
0142 dot2c is a utility that can parse a .dot file containing an automaton as
0143 in the example above and automatically convert it to the C representation
0144 presented in [3].
0145
0146 For example, having the previous 'wip' model into a file named 'wip.dot',
0147 the following command will transform the .dot file into the C
0148 representation (previously shown) in the 'wip.h' file::
0149
0150 $ dot2c wip.dot > wip.h
0151
0152 The 'wip.h' content is the code sample in section 'Deterministic Automaton
0153 in C'.
0154
0155 Remarks
0156 -------
0157
0158 The automata formalism allows modeling discrete event systems (DES) in
0159 multiple formats, suitable for different applications/users.
0160
0161 For example, the formal description using set theory is better suitable
0162 for automata operations, while the graphical format for human interpretation;
0163 and computer languages for machine execution.
0164
0165 References
0166 ----------
0167
0168 Many textbooks cover automata formalism. For a brief introduction see::
0169
0170 O'Regan, Gerard. Concise guide to software engineering. Springer,
0171 Cham, 2017.
0172
0173 For a detailed description, including operations, and application on Discrete
0174 Event Systems (DES), see::
0175
0176 Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
0177 event systems. Boston, MA: Springer US, 2008.
0178
0179 For the C representation in kernel, see::
0180
0181 De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
0182 Silva. Efficient formal verification for the Linux kernel. In:
0183 International Conference on Software Engineering and Formal Methods.
0184 Springer, Cham, 2019. p. 315-332.
