Runtime Verification deals with the question of whether a run of a system adheres to its specification. This paper studies runtime verification in the presence of partial knowledge about the observed run, particularly where input values may not be precise or may not be observed at all. We also allow declaring assumptions on the execution which permits to obtain more precise verdicts also under imprecise inputs. To this end, we show how to understand a given correctness property as a symbolic formula and explain that monitoring boils down to solving this formula iteratively, whenever more and more observations of the run are given. We base our framework on stream runtime verification, which allows to express temporal correctness properties not only in the Boolean but also in richer logical theories. While in general our approach requires to consider larger and larger sets of formulas, we identify domains (including Booleans and Linear Algebra) for which pruning strategies exist, which allows to monitor with constant memory (i.e. independent of the length of the observation) while preserving the same inference power as the monitor that remembers all observations. We empirically exhibit the power of our technique using a prototype implementation under two important cases studies: software for testing car emissions and heart-rate monitoring.
翻译:运行时间核查 涉及一个系统运行是否符合其规格的问题 。 本文研究在对所观察到运行过程的部分了解的情况下进行时间核查, 特别是输入值可能不准确或根本不可能观察到。 我们还允许在不精确的投入下宣布对执行过程的假设, 以便获得更准确的判决。 为此, 我们展示了如何将给定正确性属性理解为一种象征性的公式, 并解释说, 监测将归结为反复解决这个公式, 只要给出了对运行过程的更多观察时, 我们以流运行时间核查为基础, 不仅在布林, 而且还在更丰富的逻辑理论中显示时间正确性。 虽然我们的方法一般需要考虑更多和更多的公式, 但是我们通常需要考虑存在运行战略的领域( 包括布林恩斯和线性代格布拉 ), 以便用恒定记忆( 独立于观察的长度) 来监测, 同时保留与监测所有观测结果相同的推导力。 我们通过两个重要案例( 测试汽车排放的软件和软件), 实验性地展示了我们技术的原型执行力。