Runtime verification of real-time event streams using the tool HStriver
Pages 3 - 34
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.
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 and Schallhart C A brief account of runtime verification J Log Algebr Program 2009 78 5 293-303
[3]
Bartocci E, Falcone Y (eds) (2018) Lectures on runtime verification—introductory and advanced topics. LNCS, vol 10457. Springer, Cham
[4]
Manna Z and Pnueli A Temporal verification of reactive systems 1995 New York Springer
[5]
Bauer A, Leucker M, and Schallhart C Runtime verification for LTL and TLTL ACM Trans Softw Eng Methodol 2011 20 4 14
[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 and Havelund K Rewriting-based techniques for runtime verification Automat Softw Eng 2005 12 2 151-197
[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 and Sánchez C Stream runtime verification of real-time event-streams with the Striver language Int J Softw Tools Technol Transf 2021 23 157-183
[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.
[22]
Havelund K Rule-based runtime verification revisited Int J Softw Tools Technol Transf 2015 17 2 143-170
[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 and Huch F Runtime verification of concurrent Haskell programs Electronic notes on theoretical computer science 2005 Amsterdam Elsevier 201-216
[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, and von Hanxleden R Ahmed A Deterministic concurrency: a clock-synchronised shared memory approach Programming languages and systems 2018 Cham Springer 86-113
[35]
Talpin J-P, Brandt J, Gemünde M, Schneider K, and Shukla S Artemov S and Nerode A Constructive polychronous systems Logical foundations of computer science 2013 Berlin, Heidelberg Springer 335-349
[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
Index Terms
- Runtime verification of real-time event streams using the tool HStriver
Index terms have been assigned to the content through auto-classification.
Recommendations
Stream runtime verification of real-time event streams with the Striver language
AbstractIn this paper, we study the problem of runtime verification of real-time event streams; in particular, we propose a language to describe monitors for real-time event streams that can manipulate data from rich domains. We propose a solution based ...
HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams
Formal MethodsAbstractWe present HStriver, an extensible stream runtime verification tool for event streams. The tool consists of a runtime verification engine for (1) real-time events streams where individual observations and verdicts can occur at arbitrary times, and ...
Runtime verification of real-time event streams under non-synchronized arrival
AbstractWe study the problem of online runtime verification of real-time event streams. Our monitors can observe concurrent systems with a shared clock, but where each component reports observations as signals that arrive to the monitor at different ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature 2023. 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.
Publisher
Kluwer Academic Publishers
United States
Publication History
Published: 21 June 2023
Accepted: 16 April 2023
Received: 29 April 2022
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 17 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in