ostl3rs — OCaml STL Light Library for Reactive Systems

ostl3rs reads Signal Temporal Logic (STL/MTL) formulas over discrete time and turns them into:

• three-valued synchronous observers in Lustre, usable both for runtime monitoring (compiled with lustrec) and for formal verification (model checked with lustrec/zustre or Kind2);
• robust semantics expressions (quantitative satisfaction at time 0), for several robustness definitions.

It is both a command-line tool (ostl3rs) and an OCaml library. The lustrec compiler uses the library to verify the temporal guarantees of Lustre contracts.

Three-valued observers

A bounded future formula such as eventually[0,3] (x > 5) cannot be decided at the instant it starts: its value is only known once enough of the future has been observed. ostl3rs therefore uses a three-valued semantics (true, false, unknown) and generates, for each formula, a Lustre node with two boolean outputs:

p_true	p_false	verdict
false	false	unknown (not decided yet)
true	false	true
false	true	false

Both are never true together, and once a verdict is reached it never changes. The horizon of a formula, computed by ostl3rs, is the number of steps after which the verdict is guaranteed to be decided (e.g. 3 for eventually[0,3] p, 8 for always[0,2] eventually[3,6] p).

Example: ostl3rs r.stl with

x: int;
resp = eventually[0,3] (x > 5);

produces

#open "stl3v"

node nd_resp_tmp_2 (x: int) returns (resp_tmp_2: bool);
let
  resp_tmp_2 = x - 5 > 0;
tel

node nd_resp (x: int) returns (resp_true, resp_false: bool);
var __v: bool;
let
  __v = nd_resp_tmp_2(x);
  (resp_true, resp_false) = eventually_3v(0, 3, __v);
tel

The temporal operators (eventually_3v, always_3v, until_3v, ...) are defined in the stl3v library, share/stl3v.lus, installed with the package. Each operator comes with its contract and proof nodes; share/stl3v-proof.lus and share/run_analysis.sh re-check them with Kind2. The same library is also exposed to OCaml as the string Ostl3rs_lustre.Stl3v.source, for tools that need the bodies of its nodes.

Nested future operators

When future operators are nested (always[0,2] eventually[3,6] p), the inner observer must be evaluated from several starting instants. Four encodings are available (-future), described in doc/nested_until.tex:

• unfold: the formula is unfolded down to two-valued subformulas, latched at each step; no node is ever restarted. Best suited to model checking.
• copies: one copy of the inner observer per starting instant, each restarted once.
• fold (default): the copies are reused modulo the horizon of the inner formula.
• lagged: a single flat node for the whole formula, with an extra first input trigger: the formula is evaluated from every step where trigger holds, from delayed values of its two-valued subformulas; no node is ever restarted. <name>_false holds when an instance started at most h steps ago (h the horizon) is already false, <name>_true when the instance started h steps ago is true. Past operators are not supported yet.

test/encodings/check_encodings.sh checks with Kind2 that the encodings agree on the corpus test/encodings/corpus.stl (for lagged, against h+1 restarted copies of the unfolded observer).

Input language

A .stl file contains signal declarations and named definitions, in any order. Comments are (* ... *) and can be nested.

x, P: int;
y, z: real;
b: bool;

p = always[2,5] eventually[3,6] (P > 0);
q = (z - 1.5 > 0.0) until[0,2] (y < 2.0);
r = b since[0,1] (x >= 1 and prev b);

construct	syntax
signal types	int, real, bool
future operators	always[a,b] f, eventually[a,b] f, f until[a,b] g, next f (= eventually[1,1] f)
past operators	prev f, f since[a,b] g
boolean connectives	not, and / &&, or / ||, xor, =>, true, false
atoms	e1 > e2, <, >=, <=, =, <> on arithmetic expressions
arithmetic	+, -, *, /, unary -, int and real literals

Intervals are integer instants with 0 <= a <= b. A boolean signal is a formula on its own; int and real signals occur in atoms. Binary temporal operators bind tighter than and/or. Robust semantics are only defined for numerical signals.

Installation

With opam:

opam pin add ostl3rs git+https://github.com/Embedded-SW-VnV/ostl3rs.git

From a clone:

git clone https://github.com/Embedded-SW-VnV/ostl3rs.git
cd ostl3rs
opam install . --deps-only
dune build
dune test
dune install

Dependencies: OCaml, dune (>= 3.7), zarith, menhir. Compiling or verifying the generated Lustre code needs lustrec or Kind2.

Command line

ostl3rs [options] FILE.stl

  -lustre          Three-valued Lustre observers (default)
  -robust SEM      Robust semantics expression at time 0, SEM in
                   classic, max10, const10, add10, telex, cumulative,
                   sumproduct, summin, maxproduct, minonly, smooth_rec, smooth1
  -future ENC      Encoding of nested future operators: unfold, copies, fold, lagged
                   (default: fold)
  -kind2           Kind2 syntax for the Lustre output (default: lustrec)
  -o FILE          Write the output to FILE (default: stdout)

To compile an observer with lustrec, compile the stl3v library first:

ostl3rs -o r.lus r.stl
lustrec -d build $(opam var share)/ostl3rs/stl3v.lus
lustrec -I build -d build -m nd_resp r.lus

Library

library	modules	content
ostl3rs	Ast, Parse, Typing, Core, Transform	formulas, parsing and typing (Parse.formula_of_string, Parse.program_of_file), horizon and free variables, normalization (Transform.process_formula)
ostl3rs.lustre	ToLustre, Lustre_ir, Lustre_pp, Stl3v	Lustre observers as an IR (ToLustre.nodes_of_formula), printer (lustrec or Kind2 dialect), stl3v library source
ostl3rs.robust	Robust, Robust_quantitative_general, Robust_dgsar	robust semantics

bin/main.ml is a short example of the whole pipeline.

Tests

dune test runs the command-line regression tests (test/cli.t), the parser tests (test/parse_string.ml) and test/ostl3rs.ml. test/encodings/check_encodings.sh (requires Kind2) is not part of dune test.

License

LGPL-3.0-or-later. Author: Pierre-Loïc Garoche.