Towards proved formal specification and verification of STL operators as synchronous observers

Submission [pdf]

Proofs [pdf]

Lustre files

• Eventually [lus]
• Always [lus]
• Until [lus]

script to generate tables [sh]

Logs (here nodes are analyzed at once, while figures were reported node by node in a modular way in the paper, see build script)

• Eventually
  • proof_ev_true [log]
  • proof_ev_false [log]
  • eventually_3v [log]
• Always
  • proof_alw_true [log]
  • proof_alw_false [log]
  • always_3v [log]
• Until
  • proof_until_true [log]
  • proof_until_false [log]
  • until_3v [log]