MoCS: Monitor Circuit Synthesis

Introduction

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.

Publications

[FK09]

Bernd Finkbeiner and Lars Kuhtz. Monitor Circuits for LTL with Bounded and Unbounded Future. RV 09, 2009.

Documentation

Have a look at the README file that comes with MoCS. If you have questions please contact Lars Kuhtz.

Source Code

The source code is available at GitHub under a three-clause BSD style license.

Contact

Lars Kuhtz <kuhtzXcsYuni-sbYde> (substitute X by @ and Y by .)