[Back]

K. Selyunin, T. Nguyen, E. Bartocci, D. Nickovic, R. Grosu:
"Monitoring of MTL Specifications With IBM's Spiking-Neuron Model";
Talk: Proc. of the 2016 Design, Automation & Test in Europe Conference & Exhibition, Dresden; 2016-04-14 - 2016-04-18; in: "Proc. of the 2016 Design, Automation & Test in Europe Conference & Exhibition", IEEE Computer Society, (2016), ISBN: 978-3-9815-3707-9; 924 - 929.

This paper shows how to use the IBM's TrueNorth spiking neuron model, for monitoring if a digital signal satisfies a metric temporal-logic (MTL) specification. TrueNorth spiking neurons are universal computation blocks, which can perform a variety of deterministic or stochastic tasks (e.g., Boolean/arithmetic operations, filtering, and convolution) depending on the configuration of their parameters. We show how to set these parameters for the deterministic TrueNorth neural-model in order to recognize MTL operators. A TrueNorth circuit then behaves as a runtime MTL monitor. We demonstrate how to translate the neural monitor to synthesizable HDL-code on Xilinx's Zedboard using high-level synthesis. To the best of our knowledge, this is the first application of the IBM's TrueNorth model for runtime monitoring. It also demonstrates the complete flow from a high-level specification to the implementation of a neural monitor in FPGA. As a byproduct, the paper also introduces the first open-source FPGA implementation of the deterministic TrueNorth model. We demonstrate the usefulness of our approach on a case study, the launching of a missile from a battle ship.