MoCS: Monitor Circuit Synthesis
Copyright © 2009 Saarland Univerisity
MoCS synthesies monitor circuits from linear time temporal logic specifications. The input logic is similar to PSL by allowing nesting of regular expressions within temporal modalities. The output of MoCS is a synthesizable VHDL description of the monitor circuit. The resulting monitors implement truncated path semantics. On sequentially reading an input trace a monitor outputs at each input position whether the current prefix of the trace satisfies the monitored property. MoCS is particularly careful about generating small monitors form specifications containing sub-properties of bounded temporal scope.
|[FK09]||Bernd Finkbeiner and Lars Kuhtz. Monitor Circuits for LTL with Bounded and Unbounded Future. RV 09, 2009.|
The source code is available at GitHub under a three-clause BSD style license.
Lars Kuhtz <kuhtzXcsYuni-sbYde> (substitute X by @ and Y by .)