×

Foundations of Boolean stream runtime verification. (English) Zbl 1339.68165

Summary: Stream runtime verification (SRV), pioneered by the tool LOLA, is a declarative formalism 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 the evaluation algorithms, and 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Leucker, M.; Schallhart, C., A brief account of runtime verification, J. Log. Algebr. Program., 78, 5, 293-303, (2009) · Zbl 1192.68433
[2] Havelund, K.; Goldberg, A., Verify your runs, (Proc. of VSTTE’05, Lecture Notes in Comput. Sci., vol. 4171, (2005), Springer), 374-383
[3] Manna, Z.; Pnueli, A., Temporal verification of reactive systems safety, (1995), Springer New York
[4] Havelund, K.; Roşu, G., Synthesizing monitors for safety properties, (Proc. of TACAS’02, Lecture Notes in Comput. Sci., vol. 2280, (2002), Springer), 342-356 · Zbl 1043.68534
[5] Eisner, C.; Fisman, D.; Havlicek, J.; Lustig, Y.; McIsaac, A.; Campenhout, D. V., Reasoning with temporal logic on truncated paths, (Proc. of CAV’03, Lecture Notes in Comput. Sci., vol. 2725, (2003), Springer), 27-39 · Zbl 1278.68168
[6] Bauer, A.; Leucker, M.; Schallhart, C., Runtime verification for LTL and TLTL, ACM Trans. Softw. Eng. Methodol., 20, 4, 14, (2011)
[7] Abarbanel, Y.; Beer, I.; Gluhovsky, L.; Keidar, S.; Wolfsthal, Y., Focs - automatic generation of simulation checkers from formal specifications, (Proc. of CAV’00, Lecture Notes in Comput. Sci., vol. 1855, (2000), Springer), 538-542 · Zbl 0974.68552
[8] Sen, K.; Roşu, G., Generating optimal monitors for extended regular expressions, Electron. Notes Theor. Comput. Sci., 89, 2, 226-245, (2003)
[9] Barringer, H.; Goldberg, A.; Havelund, K.; Sen, K., Rule-based runtime verification, (Proc. of VMCAI’04, Lecture Notes in Comput. Sci., vol. 2937, (2004), Springer), 44-57 · Zbl 1202.68243
[10] Roşu, G.; Havelund, K., Rewriting-based techniques for runtime verification, Autom. Softw. Eng., 12, 2, 151-197, (2005)
[11] D’Angelo, B.; Sankaranarayanan, S.; Sánchez, C.; Robinson, W.; Finkbeiner, B.; Sipma, H. B.; Mehrotra, S.; Manna, Z., LOLA: runtime monitoring of synchronous systems, (Proc. of TIME’05, (2005), IEEE CS Press), 166-174
[12] Pnueli, A.; Zaks, A., PSL model checking and run-time verification via testers, (Proc. of FM’06, Lecture Notes in Comput. Sci., vol. 4085, (2006), Springer), 573-586
[13] Donzé, A.; Maler, O.; Bartocci, E.; Nickovic, D.; Grosu, R.; Smolka, S. A., On temporal logic and signal processing, (Proc. of ATVA’12, Lecture Notes in Comput. Sci., vol. 7561, (2012), Springer), 92-106 · Zbl 1374.68278
[14] Finkbeiner, B.; Sankaranarayanan, S.; Sipma, H. B., Collecting statistics over runtime executions, Electron. Notes Theor. Comput. Sci., 70, 4, 36-54, (2002) · Zbl 1083.68068
[15] Bauer, A.; Gore, R.; Tiu, A., A first-order policy language for history-based transaction monitoring, (Proc. of ICTAC’09, Lecture Notes in Comput. Sci., vol. 5684, (2009), Springer), 96-111 · Zbl 1250.68182
[16] Basin, D.; Harvan, M.; Klaedtke, F.; Zălinescu, E., MONPOLY: monitoring usage-control policies, (Proc. of RV’12, Lecture Notes in Comput. Sci., vol. 7687, (2012), Springer)
[17] Basin, D.; Klaedtke, F.; Müller, S., Policy monitoring in first-order temporal logic, (Proc. of CAV’10, Lecture Notes in Comput. Sci., vol. 6174, (2010), Springer), 1-18
[18] Caspi, P.; Pouzet, M., Synchronous kahn networks, (Proc. of ICFP’96, (1996), ACM Press), 226-238 · Zbl 1344.68049
[19] Berry, G., The foundations of esterel, (Proof, Language, and Interaction: Essays in Honour of Robin Milner, (2000), MIT Press), 425-454
[20] Halbwachs, N.; Caspi, P.; Pilaud, D.; Plaice, J., Lustre: a declarative language for programming synchronous systems, (Proc. of POPL’87, (1987), ACM Press), 178-188
[21] Gautier, T.; Le Guernic, P.; Besnard, L., SIGNAL: a declarative language for synchronous programming of real-time systems, (Proc. of FPCA’87, Lecture Notes in Comput. Sci., vol. 274, (1987), Springer), 257-277
[22] Pike, L.; Goodloe, A.; Morisset, R.; Niller, S., Copilot: a hard real-time runtime monitor, (Proc. of RV’10, Lecture Notes in Comput. Sci., vol. 6418, (2010), Springer)
[23] Goodloe, A. E.; Pike, L., Monitoring distributed real-time systems: a survey and future directions, (2010), Tech. rep., NASA Langley Research Center
[24] Veanes, M.; Hooimeijer, P.; Livshits, B.; Molnar, D.; Bjørner, N., Symbolic finite state transducers: algorithms and applications, (Proc. of POPL’12, (2012), ACM), 137-150 · Zbl 1321.68341
[25] D’Antoni, L.; Veanes, M., Extended symbolic finite automata and transducers, Form. Methods Syst. Des., 47, 1, 93-119, (2015) · Zbl 1341.68085
[26] Alur, R.; D’Antoni, L.; Raghothaman, M., Drex: a declarative language for efficiently evaluating regular string transformations, (Proc. of POPL’15, (2015), ACM), 125-137 · Zbl 1345.68032
[27] Pike, L.; Wegmann, N.; Niller, S.; Goodloe, A., Copilot: monitoring embedded systems, (2012), Tech. rep., NASA, NASA/CR-2012-217329
[28] Digital design, computer organization, (2004), CRC Press
[29] Wolper, P., Temporal logic can be more expressive, Inform. Control, 56, 72-99, (1983) · Zbl 0534.03009
[30] Laroussinie, F.; Markey, N.; Schnoebelen, P., Temporal logic with forgettable past, (Proc. of LICS’02, (2002), IEEE CS Press), 383-392
[31] 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, 598-611, (1985) · Zbl 0577.68074
[32] Meyer, A. R.; Stockmeyer, L. J., The equivalence problem for regular expressions with squaring requires exponential space, (Proc. of FOCS’72, (1972), IEEE CS Press), 125-129
[33] Harel, D., The spirit of computing, (1992), Addison-Wesley · Zbl 0755.68003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.