  Signal Temporal Logic (STL) is a convenient formalism to express bounded
horizon properties of autonomous critical systems. STL extends LTL to
real-valued signals and associates a non-singleton bound interval to each
temporal operators. In this work we provide a rigorous encoding of non-nested
discrete-time STL formulas into Lustre synchronous observers.
  Our encoding provides a three-valued online semantics for the observers and
therefore enables both the verification of the property and the search of
counter-examples. A key contribution of this work is an instrumented proof of
the validity of the implementation. Each node is proved correct with respect to
the original STL semantics. All the experiments are automated with the Kind2
model-checker and the Z3 SMT solver.
