RVHyper: A Runtime Verification Tool for Temporal Hyperproperties

Autor:	Finkbeiner, Bernd, Hahn, Christopher, Stenger, Marvin, Tentrup, Leander
Rok vydání:	2019
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	We present RVHyper, a runtime verification tool for hyperproperties. Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. Specifications are given as formulas in the temporal logic HyperLTL, which extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. RVHyper processes execution traces sequentially until a violation of the specification is detected. In this case, a counter example, in the form of a set of traces, is returned. As an example application, we show how RVHyper can be used to detect spurious dependencies in hardware designs. Comment: arXiv admin note: substantial text overlap with arXiv:1807.00758
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1906.00798 Zobrazit plný text záznamu View this record from Arxiv