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 条
  • [21] Pnueli A., Zaks A., PSL model checking and run-time verification via testers, FM 2006. LNCS, 4085, pp. 573-586, (2006)
  • [22] Rosu G., Havelund K., Rewriting-based techniques for runtime verification, Autom. Softw. Eng, 12, 2, pp. 151-197, (2005)
  • [23] Sen K., Rosu G., Generating optimal monitors for extended regular expressions, ENTCS, 89, 2, pp. 226-245, (2003)
  • [24] Stearns R.E., Hunt H.B., On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata, SIAM J. Comput, 14, 3, pp. 598-611, (1985)
  • [25] Veanes M., Hooimeijer P., Livshits B., Molnar D., Bjrner N., Symbolic finite state transducers: Algorithms and applications, Proc. ofPOPL 2012, pp. 137-150, (2012)