MetadataShow full item record
AbstractAbstract: Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for parametric runtime verification. Here we consider the correspondence between trace-slicing automata-based approaches and rule systems. The main contribution is a translation from quantified automata to rule systems, which has been implemented in Scala. This then allows us to highlight the key differences in how the two formalisms handle data, an important step in our wider effort to understand the correspondence between different specification languages for parametric runtime verification. This paper extends a previous conference version of this paper with further examples, a proof of correctness, and an optimisation based on a notion of redundancy observed during the development of the translation.
CitationInternational Journal on Software Tools for Technology Transfer, volume 23, issue 2, page 209-228
PublisherSpringer Berlin Heidelberg
DescriptionFrom Springer Nature via Jisc Publications Router
History: accepted 2021-01-12, registration 2021-01-13, online 2021-02-27, pub-electronic 2021-02-27, pub-print 2021-04
Publication status: Published