Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Runtime verification of real-time event streams using the tool HStriver

  • Original Article
  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We present in this paper the tool HStriver, an extensible stream runtime verification tool for monitoring real-time event streams. Real-time event streams are formed by events that contain rich data and can occur at arbitrary times. The rich expressivity of HStriver allows the specifications of quantitative semantics of logics like signal temporal logic (STL), including different notions of robustness. Stream runtime verification is a specification family of languages based on the clean separation between temporal dependencies and data computations. To encode the data values contained in the events (both read as inputs and produced as the result of computation) HStriver borrows a large subset of data-types from Haskell. These types are transparently lifted into the HStriver specification language and incorporated in the temporal engine, so they can be used as the types of the input (observations), output (verdicts), and intermediate streams. The temporal evaluation engine is agnostic of the types used in the specification. The resulting extensible language is then embedded into Haskell as an embedded Domain Specific Langauge. The availability of functional features in the specification language enables the direct implementation of desirable features in HStriver like parametrization (using functions that return stream definitions), etc. The resulting tool, HStriver, is a flexible and extensible stream runtime verification engine for real-time streams. We illustrate the use of HStriver on many sophisticated real-time specifications, including realistic STL properties of existing designs.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.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

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. An earlier short version of this paper appeared in [21].

References

  1. Havelund K, Goldberg A (2005) Verify your runs. In: Proceedings of verified software: theories, tools, and experiments (VSTTE’05), LNCS, vol 4171. Springer, Heidelberg, pp 374–383

  2. Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Program 78(5):293–303

    Article  MATH  Google Scholar 

  3. Bartocci E, Falcone Y (eds) (2018) Lectures on runtime verification—introductory and advanced topics. LNCS, vol 10457. Springer, Cham

  4. Manna Z, Pnueli A (1995) Temporal verification of reactive systems. Springer, New York

    Book  MATH  Google Scholar 

  5. Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14

    Article  Google Scholar 

  6. Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: Proceedings of the 15th international conference on computer aided verification (CAV’03). LNCS, vol 2725. Springer, Heidelberg, pp 27–39

  7. Havelund K, Roşu G (2002) Synthesizing monitors for safety properties. In: Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS’02). LNCS, vol 2280. Springer, Heidelberg, pp 342–356

  8. Sen K, Roşu G (2003) Generating optimal monitors for extended regular expressions. In: Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam

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

    Article  Google Scholar 

  10. Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: Proceedings of the 5th international conference on verification, model checking and abstract interpretation (VMCAI’04). LNCS, vol 2937. Springer, Heidelberg, pp 44–57

  11. Barringer H, Rydeheard D, Havelund K (2007) Rule systems for run-time monitoring: from Eagle to RuleR. In: Proceedings of the 7th international workshop on runtime verification (RV’07). LNCS, vol 4839. Springer, Heidelberg, pp 111–125

  12. D’Angelo B, Sankaranarayanan S, Sánchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: runtime monitoring of synchronous systems. In: Proceedings of the 12th international symposium of temporal representation and reasoning (TIME’05). IEEE CS Press, Washington DC, pp 166–174

  13. Sánchez C (2018) Online and offline stream runtime verification of synchronous systems. In: Proceedings of the 18th international conference on runtime verification (RV’18). LNCS, vol 11237. Springer, Cham, pp 138–163

  14. Berry G (2000) The foundations of Esterel. Proof, language, and interaction: essays in honour of Robin Milner. MIT Press, Cambridge, MA, pp 425–454

  15. Halbwachs N, Caspi P, Pilaud D, Plaice JA (1987) Lustre: a declarative language for programming synchronous systems. In: Proceedings of the 14th ACM symposium on principles of programming languages (POPL’87). ACM Press, New York, NY, pp 178–188

  16. Convent L, Hungerecker S, Leucker M, Scheffel T, Schmitz M, Thoma D (2018) TeSSLa: temporal stream-based specification language. In: Proceedings of the 21st. Brazilian symposium on formal methods (SBMF’18). LNCS, vol 11254. Springer, Cham

  17. Leucker M, Sánchez C, Scheffel T, Schmitz M, Schramm A (2018) TeSSLa: runtime verification of non-synchronized real-time streams. In: Proceedings of the 33rd symposium on applied computing (SAC’18). ACM Press, New York, NY

  18. Gorostiaga F, Sánchez C (2018) Striver: stream runtime verification for real-time event-streams. In: Proceedings of the 18th international conference on runtime verification (RV’18). LNCS, vol 11237. Springer, Cham, pp 282–298

  19. Faymonville P, Finkbeiner B, Schledjewski M, Schwenger M, Stenger M, Tentrup L, Hazem T (2019) StreamLAB: stream-based monitoring of cyber-physical systems. In: Proceeings of the 31st international conference on computer-aided verification (CAV’19). LNCS, vol 11561. Springer, Cham, pp 421–431

  20. Gorostiaga F, Sánchez C (2021) Stream runtime verification of real-time event-streams with the Striver language. Int J Softw Tools Technol Transf 23:157–183

    Article  Google Scholar 

  21. Gorostiaga F, Sánchez C (2021) HStriver: a very functional extensible tool for the runtime verification of real-time event streams. In: Proceedings of the 24th international symposium on formal methods (FM’21). LNCS, vol 13047. Springer, Cham, pp. 563–580. https://doi.org/10.1007/978-3-030-90870-6_30

  22. Havelund K (2015) Rule-based runtime verification revisited. Int J Softw Tools Technol Transf 17(2):143–170

    Article  Google Scholar 

  23. Barringer H, Havelund K (2011) TraceContract: a scala DSL for trace analysis. In: Proceedings of the 17th international symposium on formal methods (FM’11). LNCS, vol 6664. Springer, Heidelberg, pp. 57–72

  24. Stolz V, Huch F (2005) Runtime verification of concurrent Haskell programs. Electronic notes on theoretical computer science, vol 113. Elsevier, Amsterdam, pp 201–216

    Google Scholar 

  25. Ceresa M, Gorostiaga F, Sánchez C (2020) Declarative stream runtime verification (hLola). In: Proc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS’20). LNCS, vol 12470. Springer, Cham, pp 25–43

  26. Falcone Y, Krstic S, Reger G, Traytel D (2018) A taxonomy for classifying runtime verification tools. In: Proceedings of the 18th international conference on runtime verification (RV’18). LNCS, vol 11237. Springer, Cham, pp 241–262

  27. Reinbacher T, Rozier KY, Schumann J (2014) Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings 20th International Confer on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14). LNCS, vol 8413. Springer, Heidelberg, pp 357–372

  28. Hallé S (2016) When RV meets CEP. In: Proceedings of the 16th international conference on runtime verification (RV’16). LNCS, vol 10012. Springer, Cham, pp 68–91

  29. Hallé S, Khoury R (2017) Event stream processing with BeepBeep 3. In: Proceedings of the international workshop on competitions, usability, benchmarks, evaluation, and standardisation for runtime verification tools (RV-CUBES). Kalpa Publications in Computing. EasyChair, pp 81–88

  30. Basin D, Harva M, Klaedtke F, Zalinescu E (2011) MONPOLY: monitoring usage-control policies. In: Proceedings of the 2nd international conference on runtime verification (RV’11). LNCS, vol 7186. Springer, Heidelberg, pp 360–364

  31. Basin DA, Klaedtke F, Zalinescu E (2017) The MonPoly monitoring tool. In: Proceedings of the international workshop on competitions, usability, benchmarks, evaluation, and standardisation for runtime verification tools (RV-CUBES). Kalpa Publications in Computing. EasyChair, pp 19–28

  32. Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: Proceedings of the 1st international conference on runtime verification (RV’10). LNCS, vol 6418. Springer, Heidelberg, pp 345–359

  33. Faymonville P, Finkbeiner B, Schwenger M, Torfah H(2017) Real-time stream-based monitoring. CoRR arXiv:1711.03829

  34. Aguado J, Mendler M, Pouzet M, Roop P, von Hanxleden R (2018) Deterministic concurrency: a clock-synchronised shared memory approach. In: Ahmed A (ed) Programming languages and systems. Springer, Cham, pp 86–113

    Chapter  Google Scholar 

  35. Talpin J-P, Brandt J, Gemünde M, Schneider K, Shukla S (2013) Constructive polychronous systems. In: Artemov S, Nerode A (eds) Logical foundations of computer science. Springer, Berlin, Heidelberg, pp 335–349

    Chapter  Google Scholar 

  36. Marlow S (2010) Haskell language report

  37. Gorostiaga F, Sánchez C (2021) Nested monitors: monitors as expressions to build monitors. In: Proceedings of the 21st international conference on runtime verification (RV’21). LNCS, vol 12974. Springer, Heidelberg, pp 164–183

  38. Gorostiaga F (2022) Theory and practice of stream runtime verification for sequences and real-time event based systems. https://oa.upm.es/70504/

  39. Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Proceedings of the joint international conference on formal techniques, modelling and analysis of timed and fault-tolerant systems, and formal modelling and analysis of timed systems (FORMATS/FTRTFT 2004). LNCS, vol 3253. Springer, Heidelberg, pp 152–166

  40. Donzé A, Ferrère T, Maler O (2013) Efficient robust monitoring for STL. In: Proceedings of the 25th international conference on computer aided verification (CAV’13). LNCS, vol 8044. Springer, Heidelberg, pp 264–279

  41. Jin X, Deshmukh JV, Kapinski J, Ueda K, Butts K (2014) Powertrain control verification benchmark. In: Proceedings of the 17th international conference on hybrid systems: computation and control (HSCC’14). ACM, New York, pp 253–262

  42. Cumin J, Lefebvre G, Ramparany F, Crowley J (2017) A dataset of routine daily activities in an instrumented home. In: Proceedings of the 11th international conference on ubiquitous computing and ambient intelligence (UCAmI’17). LNCS, vol 10586. Springer, Cham, pp 413–425

Download references

Author information

Authors and Affiliations

  1. IMDEA Software Institute, Madrid, Spain

    Felipe Gorostiaga & César Sánchez

  2. Universidad Politécnica de Madrid, Madrid, Spain

    Felipe Gorostiaga

  3. CIFASIS, Rosario, Argentina

    Felipe Gorostiaga

Authors
  1. Felipe Gorostiaga
    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

Corresponding author

Correspondence to Felipe Gorostiaga.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work was funded in part by the Madrid Regional Government under project “S2018/TCS-4339 (BLOQUES-CM)”, by Spanish National Project “BOSCO (PGC2018-102210-B-100)”, and by FPU Grant FPU18/04362 granted by the Spanish Ministry of Science, Innovation and Universities.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Gorostiaga, F., Sánchez, C. Runtime verification of real-time event streams using the tool HStriver. Form Methods Syst Des 61, 3–34 (2022). https://doi.org/10.1007/s10703-023-00428-9

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-023-00428-9

Keywords

Search

Navigation