Dynamically Reprogrammable Runtime Monitors for Bounded-time MTL
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918400004980736 |
|---|---|
| author | Hebballi, Chirantan Poptani, Akash Benny, Amrutha Kalayappan, Rajshekar Chandran, Sandeep Phawade, Ramchandra |
| author_facet | Hebballi, Chirantan Poptani, Akash Benny, Amrutha Kalayappan, Rajshekar Chandran, Sandeep Phawade, Ramchandra |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_19851 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Dynamically Reprogrammable Runtime Monitors for Bounded-time MTL Hebballi, Chirantan Poptani, Akash Benny, Amrutha Kalayappan, Rajshekar Chandran, Sandeep Phawade, Ramchandra Logic in Computer Science Formal Languages and Automata Theory F.1.1; I.2.4; C.4 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. |
| title | Dynamically Reprogrammable Runtime Monitors for Bounded-time MTL |
| topic | Logic in Computer Science Formal Languages and Automata Theory F.1.1; I.2.4; C.4 |
| url | https://arxiv.org/abs/2603.19851 |