On Stream Runtime Verification and Aggregate Programming
Pages 9 - 12
Abstract
Stream Runtime Verification (SRV) has been recently proposed for monitoring input streams of data while producing output streams in response. The Aggregate Programming (AP) paradigm for collection of distributed devices has been used to implement distributed runtime verification of spatial and temporal Boolean properties. In this paper we outline how distributed SRV could be implemented by AP and the new opportunities AP could bring to the field of distributed SRV.
References
[1]
Giorgio Audrito. 2020. FCPP: an efficient and extensible Field Calculus framework. In International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS). IEEE, 153–159. https://doi.org/10.1109/ACSOS49614.2020.00037
[2]
Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Volker Stolz, and Mirko Viroli. 2021. Adaptive distributed monitors of spatial properties for cyber–physical systems. Journal of Systems and Software, 175 (2021), issn:0164-1212 https://doi.org/10.1016/j.jss.2021.110908
[3]
Giorgio Audrito, Ferruccio Damiani, Volker Stolz, Gianluca Torta, and Mirko Viroli. 2022. Distributed runtime verification by past-CTL and the field calculus. Journal of Systems and Software, 187 (2022), issn:0164-1212 https://doi.org/10.1016/j.jss.2022.111251
[4]
Giorgio Audrito, Mirko Viroli, Ferruccio Damiani, Danilo Pianini, and Jacob Beal. 2019. A Higher-Order Calculus of Computational Fields. ACM Trans. Comput. Logic, 20, 1 (2019), Article 5, 55 pages. issn:1529-3785 https://doi.org/10.1145/3285956
[5]
Roberto Casadei, Mirko Viroli, Giorgio Audrito, Danilo Pianini, and Ferruccio Damiani. 2021. Engineering collective intelligence at the edge with aggregate processes. Eng. Appl. Artif. Intell., 97 (2021), 104081.
[6]
Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. 2014. Specifying and Verifying Properties of Space. In 8th IFIP International Conference in Theoretical Computer Science (TCS), Josep Díaz, Ivan Lanese, and Davide Sangiorgi (Eds.) (Lecture Notes in Computer Science, Vol. 8705). Springer, 222–235. https://doi.org/10.1007/978-3-662-44602-7_18
[7]
B. D’Angelo, S. Sankaranarayanan, C. Sanchez, W. Robinson, B. Finkbeiner, H.B. Sipma, S. Mehrotra, and Z. Manna. 2005. LOLA: runtime monitoring of synchronous systems. In 12th International Symposium on Temporal Representation and Reasoning (TIME’05). 166–174. https://doi.org/10.1109/TIME.2005.26
[8]
Luis Miguel Danielsson and César Sánchez. 2019. Decentralized Stream Runtime Verification. In Runtime Verification, Bernd Finkbeiner and Leonardo Mariani (Eds.). Springer International Publishing, Cham. 185–201. isbn:978-3-030-32079-9
[9]
Luis Miguel Danielsson and César Sánchez. 2023. Decentralized Stream Runtime Verification for Timed Asynchronous Networks. arxiv:2302.00506.
[10]
Peter Faymonville, Bernd Finkbeiner, Maximilian Schwenger, and Hazem Torfah. 2019. Real-time Stream-based Monitoring. arxiv:1711.03829.
[11]
Nicola Gigante, Angelo Montanari, and Mark Reynolds. 2017. A One-Pass Tree-Shaped Tableau for LTL+Past. In Logic for Programming, Artificial Intelligence and Reasoning (LPAR) (EPiC Series in Computing, Vol. 46). EasyChair, 456–473. http://www.easychair.org/publications/paper/340363
[12]
Felipe Gorostiaga and César Sánchez. 2021. Stream runtime verification of real-time event streams with the Striver language. Int. J. Softw. Tools Technol. Transf., 23, 2 (2021), 157–183. https://doi.org/10.1007/s10009-021-00605-3
[13]
Mirko Viroli, Jacob Beal, Ferruccio Damiani, Giorgio Audrito, Roberto Casadei, and Danilo Pianini. 2019. From distributed coordination to field calculus and aggregate computing. J. Log. Algebraic Methods Program., 109 (2019), https://doi.org/10.1016/j.jlamp.2019.100486
Index Terms
- On Stream Runtime Verification and Aggregate Programming
Recommendations
Combining Static and Runtime Verification with AC and Coq
VORTEX 2023: Proceedings of the 6th International Workshop on Verification and Monitoring at Runtime ExecutionThe importance of monitoring groups of devices working together towards shared global objectives is growing, for instance when they are used for crucial purposes like search and rescue operations during emergencies. Effective approaches in this ...
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 ...
Adding State to Stream Runtime Verification
Runtime VerificationAbstractStream Runtime Verification (SRV) is gaining traction for monitoring systems with data streams, but it struggles with specifying state-based systems and control flow. While automata models like state charts excel at representing states, functional ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2023 Owner/Author.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 July 2023
Check for updates
Author Tags
Qualifiers
- Extended-abstract
Conference
VORTEX '23
Sponsor:
VORTEX '23: 6th International Workshop on Verification and Monitoring at Runtime Execution
July 18, 2023
WA, Seattle, USA
Upcoming Conference
ISSTA '25
- Sponsor:
- sigsoft
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 50Total Downloads
- Downloads (Last 12 months)18
- Downloads (Last 6 weeks)0
Reflects downloads up to 27 Dec 2024
Other Metrics
Citations
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