AllenRV: an Extensible Monitor for Multiple Complex Specifications with High Reactivity

Abstract : AllenRV is a tool for monitoring temporal specifications, designed for ensuring good scalability in terms of size and number of formulae, and high reactivity. Its features reflect this design goal. For ensuring scalability in the number of formulae, it can simultaneously monitor a set of formulae written in past and future, next-free LTL, with some metric extensions; their efficient simultaneous monitoring is supported by a let construct allowing to share computations between formulae. For ensuring scalability in the size of formulae, it allows defining new abstractions as user-defined operators, which take discrete time boolean signals as arguments, but also constant parameters such as delays. For ensuring high reactivity, its monitoring algorithm does not require clock tick events, unlike many other tools. This is achieved by recomputing output signals both upon input signals changes and upon internally generated timeout events relative to such changes. As a consequence, monitoring remains efficient on arbitrarily fine-grained time domains. AllenRV is implemented by extending the existing Allen language and compiler, initially targeting ubiquitous applications using binary sensors, with temporal logic operators and a comprehensive library of user-defined operators on top of them. The most complex of these operators, including a complete adaptation of Allen-logic relations as selection operators, are proven correct with respect to their defined semantics. Thus, AllenRV offers an open platform for cooperatively developing increasingly complex libraries of high level, general or domain-specific, temporal operators and abstractions, without compromising correctness.
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-02272611
Contributor : Eugene Volanschi <>
Submitted on : Wednesday, August 28, 2019 - 2:38:46 PM
Last modification on : Wednesday, October 2, 2019 - 10:41:52 AM

File

tool-final-20190722-fixed.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02272611, version 2

Citation

Nic Volanschi, Bernard Serpette. AllenRV: an Extensible Monitor for Multiple Complex Specifications with High Reactivity. RV 2019 - The 19th International Conference on Runtime Verification, Oct 2019, Porto, Portugal. ⟨hal-02272611v2⟩

Share

Metrics

Record views

35

Files downloads

390