Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dynamically Reprogrammable Runtime Monitors for Bounded-time MTL

Chirantan Hebballi, Akash Poptani, Amrutha Benny, Rajshekar Kalayappan, Sandeep Chandran, Ramchandra Phawade

Abstract

A Runtime Verification (RV) framework that supports online, at-speed verification of properties that can change dynamically (during in-field operations) will benefit a large variety of applications. Several state-of-the-art RV frameworks propose to implement monitors on FPGAs. While this approach can support changes to the property being monitored during in-field operations, they struggle to keep pace with the system under verification which use high-performance processors. In this work, we propose a novel, reprogrammable monitor that is implemented using standard cells instead of FPGAs. This allows the monitor to be co-located with the system under verification (on the same die), and hence is amenable to at-speed monitoring of properties. Our proposed design consists of a programmable unit that implements five basic operations and a set of queue-update rules. We show that a composition of such programmable units faithfully implements discrete time, bounded MTL. We demonstrate through simulations that our proposed monitor can be reprogrammed (through its I/O pins) post deployment. A fairly large monitor which can support MTL formulae upto 16 atomic propositions occupies only 0.55 mm^2, while operating at a frequency of 1.25 GHz.

Dynamically Reprogrammable Runtime Monitors for Bounded-time MTL

Abstract

A Runtime Verification (RV) framework that supports online, at-speed verification of properties that can change dynamically (during in-field operations) will benefit a large variety of applications. Several state-of-the-art RV frameworks propose to implement monitors on FPGAs. While this approach can support changes to the property being monitored during in-field operations, they struggle to keep pace with the system under verification which use high-performance processors. In this work, we propose a novel, reprogrammable monitor that is implemented using standard cells instead of FPGAs. This allows the monitor to be co-located with the system under verification (on the same die), and hence is amenable to at-speed monitoring of properties. Our proposed design consists of a programmable unit that implements five basic operations and a set of queue-update rules. We show that a composition of such programmable units faithfully implements discrete time, bounded MTL. We demonstrate through simulations that our proposed monitor can be reprogrammed (through its I/O pins) post deployment. A fairly large monitor which can support MTL formulae upto 16 atomic propositions occupies only 0.55 mm^2, while operating at a frequency of 1.25 GHz.
Paper Structure (18 sections, 4 theorems, 1 equation, 5 figures, 6 tables, 1 algorithm)

This paper contains 18 sections, 4 theorems, 1 equation, 5 figures, 6 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries and Related Work
  3. Metric Temporal Logic (MTL)
  4. Related works
  5. Abstract Machines for MTL Formulae
  6. AM and its operations
  7. Realization of Evaluator Machines for MTL operators
  8. Correctness of Evaluator Machines
  9. Monitors for MTL Formulae
  10. Programmable MTL Monitor
  11. Processing Element
  12. Que
  13. Programmable Interconnects
  14. Monitor Programming
  15. Tool Description and Evaluation
  16. ...and 3 more sections

Key Result

Theorem 1

Let $\phi$ be a single-operator MTL formula and $\odot$ be the operator in it. Then in an EM for $\phi$, for all time instances $i$, with $i \geq l(\odot)$,

Figures (5)

  • Figure 1:
  • Figure 2: Architecture of the proposed MTL monitor (for $N=4$)
  • Figure 3: Architecture of a (a) Processing Element, and (b) Que
  • Figure 4: Simulation showing the MTL monitor being reprogrammed at runtime
  • Figure 5:

Theorems & Definitions (15)

  • Definition 1
  • Example 1
  • Example 2
  • Theorem 1
  • Theorem 2
  • Corollary 1
  • Proposition 1
  • Example 3
  • proof : $\phi =\neg \alpha$
  • proof : $\phi = \alpha \wedge \beta$
  • ...and 5 more