Foundations of boolean stream runtime verification

被引：9
作者：
Bozzelli, Laura [1 ]
Sánchez, CéSar [2 ,3 ]
机构：
[1] Technical University of Madrid (UPM), Madrid
[2] IMDEA Software Institute, Madrid
[3] Institute for Information Security, CSIC
来源：
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8734卷
关键词：
Specifications;
D O I：
10.1007/978-3-319-11164-3_6
中图分类号：
学科分类号：
摘要：
Stream runtime verification (SRV), pioneered by the tool LOLA, is a declarative approach to specify synchronous monitors. In SRV, monitors are described by specifying dependencies between output streams of values and input streams of values. The declarative nature of SRV enables a separation between (1) the evaluation algorithms, and (2) the monitor storage and its individual updates. This separation allows SRV to be lifted from conventional failure monitors into richer domains to collect statistics of traces. Moreover, SRV allows to easily identify specifications that can be efficiently monitored online, and to generate efficient schedules for offline monitors. In spite of these attractive features, many important theoretical problems about SRV are still open. In this paper, we address complexity, expressiveness, succinctness, and closure issues for the subclass of Boolean SRV (BSRV) specifications. Additionally, we show that for this subclass, offline monitoring can be performed with only two passes (one forward and one backward) over the input trace in spite of the alternation of past and future references in the BSRV specification. © Springer International Publishing Switzerland 2014.
引用
收藏
页码：64 / 79
页数：15
相关论文
共 25 条
  • [1] Barringer H., Goldberg A., Havelund K., Sen K., Rule-based runtime verification, VMCAI 2004. LNCS, 2937, pp. 44-57, (2004)
  • [2] Basin D., Harvan M., Klaedtke F., Zalinescu E., MONPOLY: Monitoring usagecontrol policies, RV 2011. LNCS, 7186, pp. 360-364, (2012)
  • [3] Basin D., Klaedtke F., Muller S., Policy monitoring in first-order temporal logic, CAV 2010. LNCS, 6174, pp. 1-18, (2010)
  • [4] Bauer A., Gore R., Tiu A., A first-order policy language for history-based transaction monitoring, ICTAC 2009. LNCS, 5684, pp. 96-111, (2009)
  • [5] Bauer A., Leucker M., Schallhart C., Runtime verification for LTL and TLTL, ACM Transactions on Software Engineering and Methodology, 20, 4, (2011)
  • [6] Berry G., The foundations of Esterel, Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 425-454, (2000)
  • [7] Caspi P., Pouzet M., Synchronous Kahn Networks, Proc. of ICFP 1996, pp. 226-238., (1996)
  • [8] D'angelo B., Sankaranarayanan S., Sanchez C., Robinson W., Finkbeiner B., Sipma H.B., Mehrotra S., Manna Z., LOLA: Runtime monitoring of synchronous systems, Proc. of TIME 2005, pp. 166-174, (2005)
  • [9] Eisner C., Fisman D., Havlicek J., Lustig Y., McIsaac A., Van Campenhout D., Reasoning with temporal logic on truncated paths, CAV 2003. LNCS, 2725, pp. 27-39, (2003)
  • [10] Finkbeiner B., Sankaranarayanan S., Sipma H.B., Collecting statistics over runtime executions, ENTCS, 70, 4, pp. 36-54, (2002)
123