An Algebraic Framework for Runtime Verification
An Algebraic Framework for Runtime Verification
复制标题
DOI：
10.1109/tcad.2018.2858460
复制
发表时间：
2018-11-01
影响因子：
2.9
通讯作者：
Nickovic, Dejan
中科院分区：
文献类型：
--
作者：
Jaksic, Stefan;Bartocci, Ezio;Nickovic, Dejan
运行时验证（RV）是一种务实而可扩展但严格的技术，可评估复杂系统的正确性，包括网络物理系统（CPSS）。现代的RV工具还允许测量CPS行为与给定正式要求的距离，从而量化CPS在物理环境引起的扰动方面的鲁棒性。在本文中，我们提出了代数RV（ARV），这是一个通用的语义框架，用于正确性和稳健性监测。 ARV实现了一种抽象监视程序，其中规范语言（STL）可以通过各种定性和定量语义实例化。这使我们能够通过将监视算法与STL及其语义的具体选择分开，从而揭示RV的核心方面。我们在汽车领域的两个示例中证明了框架的有效性。
Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPSs). Modern RV tools also allow to measure the distance of a CPS behavior from a given formal requirement, thus, to quantify the robustness of a CPS with respect to perturbations caused by the physical environment. In this paper, we propose algebraic RV (ARV), a general, semantic framework for correctness and robustness monitoring. ARV implements an abstract monitoring procedure, in which the specification language (STL) can be instantiated with various qualitative and quantitative semantics. This allows us to expose the core aspects of RV, by separating the monitoring algorithm from the concrete choice of the STL and its semantics. We demonstrate the effectiveness of our framework on two examples from the automotive domain.