linear_temporal_logic.rst

  1Linear temporal logic
  2=====================
  3
  4Introduction
  5------------
  6
  7Runtime verification monitor is a verification technique which checks that the
  8kernel follows a specification. It does so by using tracepoints to monitor the
  9kernel's execution trace, and verifying that the execution trace sastifies the
 10specification.
 11
 12Initially, the specification can only be written in the form of deterministic
 13automaton (DA).  However, while attempting to implement DA monitors for some
 14complex specifications, deterministic automaton is found to be inappropriate as
 15the specification language. The automaton is complicated, hard to understand,
 16and error-prone.
 17
 18Thus, RV monitors based on linear temporal logic (LTL) are introduced. This type
 19of monitor uses LTL as specification instead of DA. For some cases, writing the
 20specification as LTL is more concise and intuitive.
 21
 22Many materials explain LTL in details. One book is::
 23
 24  Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
 25  Press, 2008.
 26
 27Grammar
 28-------
 29
 30Unlike some existing syntax, kernel's implementation of LTL is more verbose.
 31This is motivated by considering that the people who read the LTL specifications
 32may not be well-versed in LTL.
 33
 34Grammar:
 35    ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
 36
 37Operands (opd):
 38    true, false, user-defined names consisting of upper-case characters, digits,
 39    and underscore.
 40
 41Unary Operators (unop):
 42    always
 43    eventually
 44    next
 45    not
 46
 47Binary Operators (binop):
 48    until
 49    and
 50    or
 51    imply
 52    equivalent
 53
 54This grammar is ambiguous: operator precedence is not defined. Parentheses must
 55be used.
 56
 57Example linear temporal logic
 58-----------------------------
 59.. code-block::
 60
 61   RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA)
 62
 63means: if it is raining, going outside means having an umbrella.
 64
 65.. code-block::
 66
 67   RAIN imply (WET until not RAIN)
 68
 69means: if it is raining, it is going to be wet until the rain stops.
 70
 71.. code-block::
 72
 73   RAIN imply eventually not RAIN
 74
 75means: if it is raining, rain will eventually stop.
 76
 77The above examples are referring to the current time instance only. For kernel
 78verification, the `always` operator is usually desirable, to specify that
 79something is always true at the present and for all future. For example::
 80
 81    always (RAIN imply eventually not RAIN)
 82
 83means: *all* rain eventually stops.
 84
 85In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and `WET` are the
 86"atomic propositions".
 87
 88Monitor synthesis
 89-----------------
 90
 91To synthesize an LTL into a kernel monitor, the `rvgen` tool can be used:
 92`tools/verification/rvgen`. The specification needs to be provided as a file,
 93and it must have a "RULE = LTL" assignment. For example::
 94
 95    RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))
 96
 97which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED` or
 98`CRASHED`.
 99
100The LTL can be broken down using sub-expressions. The above is equivalent to:
101
102   .. code-block::
103
104    RULE = always (ACQUIRE imply (ALIVE until RELEASE))
105    ALIVE = not KILLED and not CRASHED
106
107From this specification, `rvgen` generates the C implementation of a Buchi
108automaton - a non-deterministic state machine which checks the satisfiability of
109the LTL. See Documentation/trace/rv/monitor_synthesis.rst for details on using
110`rvgen`.
111
112References
113----------
114
115One book covering model checking and linear temporal logic is::
116
117  Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
118  Press, 2008.
119
120For an example of using linear temporal logic in software testing, see::
121
122  Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury.
123  2022. Linear-time temporal logic guided greybox fuzzing. In Proceedings of the
124  44th International Conference on Software Engineering (ICSE '22).  Association
125  for Computing Machinery, New York, NY, USA, 1343–1355.
126  https://doi.org/10.1145/3510003.3510082
127
128The kernel's LTL monitor implementation is based on::
129
130  Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly
131  Automatic Verification of Linear Temporal Logic. In: Dembiński, P., Średniawa,
132  M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP
133  Advances in Information and Communication Technology. Springer, Boston, MA.
134  https://doi.org/10.1007/978-0-387-34892-6_1