SpringerLink
Log in

Foundations of Boolean Stream Runtime Verification

  • Conference paper
Runtime Verification (RV 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8734))

Included in the following conference series:

  • 1343 Accesses

Abstract

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.

This work was funded in part by Spanish MINECO Project “TIN2012-39391-C04-01 STRONGSOFT” and by Spanish MINECO Project “TIN2012-38137-C02 VIVAC”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Spain)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (Spain)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 51.99
Price includes VAT (Spain)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: MONPOLY: Monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 360–364. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Basin, D., Klaedtke, F., Müller, S.: Policy monitoring in first-order temporal logic. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 1–18. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Bauer, A., Goré, R., Tiu, A.: A first-order policy language for history-based transaction monitoring. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 96–111. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology 20(4), 14 (2011)

    Article  Google Scholar 

  6. Berry, G.: The foundations of Esterel. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 425–454. MIT Press (2000)

    Google Scholar 

  7. Caspi, P., Pouzet, M.: Synchronous Kahn Networks. In: Proc. of ICFP 1996, pp. 226–238. ACM Press (1996)

    Google Scholar 

  8. 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. In: Proc. of TIME 2005, pp. 166–174. IEEE CS Press (2005)

    Google Scholar 

  9. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Finkbeiner, B., Sankaranarayanan, S., Sipma, H.B.: Collecting statistics over runtime executions. ENTCS 70(4), 36–54 (2002)

    Google Scholar 

  11. Gautier, T., Le Guernic, P., Besnard, L.: SIGNAL: A declarative language for synchronous programming of real-time systems. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 257–277. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  12. Goodloe, A.E., Pike, L.: Monitoring distributed real-time systems: A survey and future directions. Technical report, NASA Langley Research Center (2010)

    Google Scholar 

  13. Halbwachs, N., Caspi, P., Pilaud, D., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: Proc. of POPL 1987, pp. 178–188. ACM Press (1987)

    Google Scholar 

  14. Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) Verified Software. LNCS, vol. 4171, pp. 374–383. Springer, Heidelberg (2008)

    Google Scholar 

  15. Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proc. of LICS 2002, pp. 383–392. IEEE CS Press (2002)

    Google Scholar 

  17. Leucker, M., Schallhart, C.: A brief account of runtime verification. The Journal of Logic and Algebraic Programming 78(5), 293–303 (2009)

    Article  MATH  Google Scholar 

  18. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)

    Book  Google Scholar 

  19. Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: Proc. of FOCS 1972, pp. 125–129. IEEE CS Press (1972)

    Google Scholar 

  20. Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: A hard real-time runtime monitor. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 345–359. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151–197 (2005)

    Article  Google Scholar 

  23. Sen, K., Roşu, G.: Generating optimal monitors for extended regular expressions. ENTCS 89(2), 226–245 (2003)

    Google Scholar 

  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), 598–611 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  25. Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjrner, N.: Symbolic finite state transducers: algorithms and applications. In: Proc. of POPL 2012, pp. 137–150. ACM (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Madrid (UPM), Madrid, Spain

    Laura Bozzelli

  2. IMDEA Software Institute, Madrid, Spain

    César Sánchez

  3. Institute for Information Security, CSIC, Spain

    César Sánchez

Authors
  1. Laura Bozzelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. César Sánchez
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4L7, Hamilton, ON, Canada

    Borzoo Bonakdarpour

  2. Department of Computer Science, State University of New York at Stony Brook, 1423 Computer Science, 11794-4400, Stony Brook, NY, USA

    Scott A. Smolka

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Bozzelli, L., Sánchez, C. (2014). Foundations of Boolean Stream Runtime Verification. In: Bonakdarpour, B., Smolka, S.A. (eds) Runtime Verification. RV 2014. Lecture Notes in Computer Science, vol 8734. Springer, Cham. https://doi.org/10.1007/978-3-319-11164-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11164-3_6

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11163-6

  • Online ISBN: 978-3-319-11164-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation