Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I
复制标题
计算机辅助验证 - 第 27 届国际会议，CAV 2015，美国加利福尼亚州旧金山，2015 年 7 月 18-24 日，会议记录，第一部分
DOI：
10.1007/978-3-319-21690-4_17
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Grigore R
中科院分区：
文献类型：
--
作者：
Grigore R
在运行时验证中，核心问题是判断给定的程序执行是否违反了给定的属性。在在线运行时验证中，监视器观察程序的执行情况。如果被观察的程序具有硬实时约束，那么监视器将继承它们。在硬实时约束的存在下，如果观察到违反属性，则保持足够的信息以产生错误跟踪就成为一个挑战。在本文中，我们介绍了一种数据结构，称为树缓冲区，解决了这个问题的背景下，基于自动机的监视器：如果监视器本身尊重硬实时约束，然后丰富它的树缓冲区，使它能够提供错误的痕迹，这是必不可少的诊断缺陷。我们表明，树缓冲区在其他应用领域也是有用的。例如，它们可以用来实现在正则表达式中捕获组的功能。我们证明了我们的数据结构的最佳渐近界，并验证他们使用经验数据从两个来源：通过维基百科的正则表达式搜索，并从DaCapo测试套件获得的执行痕迹的运行时验证。
Inruntime verification, the central problem is to decide if a given program execution violates a given property. Inonlineruntime verification, a monitor observes a program’s execution as it happens. If the program being observed has hard real-time constraints, then the monitor inherits them. In the presence of hard real-time constraints it becomes a challenge to maintain enough information to produceerror traces, should a property violation be observed. In this paper we introduce a data structure, calledtree buffer, that solves this problem in the context of automata-based monitors: If the monitor itself respects hard real-time constraints, then enriching it by tree buffers makes it possible to provide error traces, which are essential for diagnosing defects. We show that tree buffers are also useful in other application domains. For example, they can be used to implement functionality ofcapturing groupsin regular expressions. We prove optimal asymptotic bounds for our data structure, and validate them using empirical data from two sources: regular expression searching through Wikipedia, and runtime verification of execution traces obtained from the DaCapo test suite.