research-article

Open access

Optimising Aggregate Monitors for Spatial Logic of Closure Spaces Properties

Authors:

Gianluca Aguzzi,

Giorgio Audrito,

Mirko ViroliAuthors Info & Claims

VORTEX 2024: Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution

Pages 25 - 31

https://doi.org/10.1145/3679008.3685544

Published: 13 September 2024 Publication History

Abstract

The advent of highly distributed systems, such as the Internet of Things, has led to the development of distributed systems that require efficient and resilient runtime monitoring. Among the various monitoring techniques, runtime verification is a lightweight verification method that assesses the correctness of a running system concerning a formal specification. In this paper, we investigate the optimization of aggregate monitors, i.e., monitors that operate on ensembles of devices, for properties expressed in Spatial Logic of Closure Spaces (SLCS)--a formal logic designed to reason about spatial relationships between entities in a distributed system. We propose three different algorithms for the implementation of the "somewhere" operator, a key construct in SLCS, and we evaluate their performance through a series of simulations, comparing their convergence time and computational load.

References

[1]

Gianluca Aguzzi, Roberto Casadei, Niccolò Maltoni, Danilo Pianini, and Mirko Viroli. 2021. ScaFi-Web: A Web-Based Application for Field-Based Coordination Programming. In Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, Ferruccio Damiani and Ornela Dardha (Eds.) (Lecture Notes in Computer Science, Vol. 12717). Springer, 285–299. https://doi.org/10.1007/978-3-030-78142-2_18

Digital Library

[2]

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

[3]

Giorgio Audrito, Jacob Beal, Ferruccio Damiani, and Mirko Viroli. 2018. Space-Time Universality of Field Calculus. In Coordination Models and Languages (COORDINATION) (Lecture Notes in Computer Science, Vol. 10852). Springer, 1–20. https://doi.org/10.1007/978-3-319-92408-3_1

Digital Library

[4]

Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Guido Salvaneschi, and Mirko Viroli. 2024. The eXchange Calculus (XC): A functional programming language design for distributed collective systems. J. Syst. Softw., 210 (2024), 111976. https://doi.org/10.1016/J.JSS.2024.111976

Digital Library

[5]

Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Volker Stolz, and Mirko Viroli. 2021. Adaptive distributed monitors of spatial properties for cyber-physical systems. J. Syst. Softw., 175 (2021), https://doi.org/10.1016/j.jss.2021.110908

[6]

Giorgio Audrito, Ferruccio Damiani, Giuseppe Martino Di Giuda, Silvia Meschini, Laura Pellegrini, Elena Seghezzi, Lavinia Chiara Tagliabue, Lorenzo Testa, and Gianluca Torta. 2021. RM for users’ safety and security in the built environment. In VORTEX 2021: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution, Virtual Event, Denmark, 12 July 2021, Wolfgang Ahrendt, Davide Ancona, and Adrian Francalanza (Eds.). ACM, 13–16. https://doi.org/10.1145/3464974.3468445

Digital Library

[7]

Giorgio Audrito, Ferruccio Damiani, Volker Stolz, Gianluca Torta, and Mirko Viroli. 2022. Distributed runtime verification by past-CTL and the field calculus. J. Syst. Softw., 187 (2022), https://doi.org/10.1016/j.jss.2022.111251

Digital Library

[8]

Giorgio Audrito, Ferruccio Damiani, and Gianluca Torta. 2022. Bringing Aggregate Programming Towards the Cloud. In Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part III, Tiziana Margaria and Bernhard Steffen (Eds.) (Lecture Notes in Computer Science, Vol. 13703). Springer, 301–317. https://doi.org/10.1007/978-3-031-19759-8_19

Digital Library

[9]

Giorgio Audrito, Ferruccio Damiani, and Gianluca Torta. 2024. Real-Time Guarantees for SLCS Monitors in XC. In VORTEX 2024: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution. ACM. https://doi.org/10.1145/3679008.3685545

Digital Library

[10]

Giorgio Audrito, Luigi Rapetta, and Gianluca Torta. 2022. Extensible 3D Simulation of Aggregated Systems with FCPP. In Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13-17, 2022, Proceedings, Maurice H. ter Beek and Marjan Sirjani (Eds.) (Lecture Notes in Computer Science, Vol. 13271). Springer, 55–71. https://doi.org/10.1007/978-3-031-08143-9_4

Digital Library

[11]

Giorgio Audrito and Gianluca Torta. 2021. Towards aggregate monitoring of spatio-temporal properties. In VORTEX 2021: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution, Virtual Event, Denmark, 12 July 2021, Wolfgang Ahrendt, Davide Ancona, and Adrian Francalanza (Eds.). ACM, 26–29. https://doi.org/10.1145/3464974.3468448

Digital Library

[12]

Giorgio Audrito and Gianluca Torta. 2024. FCPP to aggregate them all. Sci. Comput. Program., 231 (2024), 103026. https://doi.org/10.1016/J.SCICO.2023.103026

Digital Library

[13]

Jacob Beal, Stefan Dulman, Kyle Usbeck, Mirko Viroli, and Nikolaus Correll. 2013. Organizing the Aggregate: Languages for Spatial Computing. In Formal and Practical Aspects of Domain-Specific Languages: Recent Developments. IGI Global, 436–501. isbn:978-1-4666-2092-6 https://doi.org/10.4018/978-1-4666-2092-6.ch016

[14]

Jacob Beal, Danilo Pianini, and Mirko Viroli. 2015. Aggregate Programming for the Internet of Things. IEEE Computer, 48, 9 (2015), 22–30. isbn:1471-2962 issn:1364-503X https://doi.org/10.1109/MC.2015.261

Digital Library

[15]

Pierfrancesco Bellini, R. Mattonlini, and Paolo Nesi. 2000. Temporal logics for real-time system specification. ACM Comput. Surv., 32, 1 (2000), 12–42. https://doi.org/10.1145/349194.349197

Digital Library

[16]

Marc Carwehl, Thomas Vogel, Genaína Nunes Rodrigues, and Lars Grunske. 2024. Runtime Verification of Self-Adaptive Systems with Changing Requirements. In Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26 - March 1, 2024, Rick Rabiser, Manuel Wimmer, Iris Groher, Andreas Wortmann, and Bianca Wiesmayr (Eds.) (LNI, Vol. P-343). Gesellschaft für Informatik e.V., 151–152. https://doi.org/10.18420/SW2024_50

[17]

Roberto Casadei. 2023. Macroprogramming: Concepts, State of the Art, and Opportunities of Macroscopic Behaviour Modelling. ACM Comput. Surv., 55, 13s (2023), 275:1–275:37. https://doi.org/10.1145/3579353

Digital Library

[18]

Roberto Casadei, Mirko Viroli, Gianluca Aguzzi, and Danilo Pianini. 2022. ScaFi: A Scala DSL and Toolkit for Aggregate Programming. SoftwareX, 20 (2022), 101248. https://doi.org/10.1016/J.SOFTX.2022.101248

[19]

Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. 2016. Model Checking Spatial Logics for Closure Spaces. Log. Methods Comput. Sci., 12, 4 (2016), https://doi.org/10.2168/LMCS-12(4:2)2016

[20]

Yliès Falcone, Srdan Krstic, Giles Reger, and Dmitriy Traytel. 2021. A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf., 23, 2 (2021), 255–284. https://doi.org/10.1007/S10009-021-00609-Z

Digital Library

[21]

Adrian Francalanza, Jorge A. Pérez, and César Sánchez. 2018. Runtime Verification for Decentralised and Distributed Systems. In Lectures on Runtime Verification - Introductory and Advanced Topics (Lecture Notes in Computer Science, Vol. 10457). Springer, 176–210. https://doi.org/10.1007/978-3-319-75632-5_6

[22]

Klaus Havelund and Grigore Rosu. 2004. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods Syst. Des., 24, 2 (2004), 189–215. https://doi.org/10.1023/B:FORM.0000017721.39909.4B

Digital Library

[23]

Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 21, 7 (1978), 558–565.

Digital Library

[24]

K. Rustan M. Leino. 2013. Developing verified programs with dafny. In 35th International Conference on Software Engineering, ICSE ’13, San Francisco, CA, USA, May 18-26, 2013, David Notkin, Betty H. C. Cheng, and Klaus Pohl (Eds.). IEEE Computer Society, 1488–1490. https://doi.org/10.1109/ICSE.2013.6606754

[25]

Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification. J. Log. Algebr. Program., 78, 5 (2009), 293–303. https://doi.org/10.1016/j.jlap.2008.08.004

[26]

Kenneth L. McMillan and Oded Padon. 2020. Ivy: A Multi-modal Verification Tool for Distributed Algorithms. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, Shuvendu K. Lahiri and Chao Wang (Eds.) (Lecture Notes in Computer Science, Vol. 12225). Springer, 190–202. https://doi.org/10.1007/978-3-030-53291-8_12

Digital Library

[27]

Yuanqiu Mo, Giorgio Audrito, Soura Dasgupta, and Jacob Beal. 2022. Near-optimal knowledge-free resilient leader election. Autom., 146 (2022), 110583. https://doi.org/10.1016/J.AUTOMATICA.2022.110583

Digital Library

[28]

Danilo Pianini, Jacob Beal, and Mirko Viroli. 2016. Improving Gossip Dynamics Through Overlapping Replicates. In Coordination Models and Languages - 18th IFIP WG 6.1 International Conference, COORDINATION 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, Alberto Lluch-Lafuente and José Proença (Eds.) (Lecture Notes in Computer Science, Vol. 9686). Springer, 192–207. https://doi.org/10.1007/978-3-319-39519-7_12

[29]

Danilo Pianini, Sara Montagna, and Mirko Viroli. 2013. Chemical-oriented simulation of computational systems with ALCHEMIST. J. Simulation, 7, 3 (2013), 202–215. https://doi.org/10.1057/jos.2012.27

[30]

Danilo Pianini, Mirko Viroli, and Jacob Beal. 2015. Protelis: Practical Aggregate Programming. In ACM Symposium on Applied Computing (SAC). 1846–1853. https://doi.org/10.1145/2695664.2695913

Digital Library

[31]

César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliès Falcone, Adrian Francalanza, Srdan Krstic, João M. Lourenço, Dejan Nickovic, Gordon J. Pace, José Rufino, Julien Signoles, Dmitriy Traytel, and Alexander Weiss. 2019. A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des., 54, 3 (2019), 279–335. https://doi.org/10.1007/S10703-019-00337-W

[32]

Mirko Viroli, Giorgio Audrito, Jacob Beal, Ferruccio Damiani, and Danilo Pianini. 2018. Engineering Resilient Collective Adaptive Systems by Self-Stabilisation. ACM Trans. Model. Comput. Simul., 28, 2 (2018), 1–16. issn:1049-3301

Digital Library

[33]

Mirko Viroli, Jacob Beal, Ferruccio Damiani, Giorgio Audrito, Roberto Casadei, and Danilo Pianini. 2018. From Field-Based Coordination to Aggregate Computing. In Coordination Models and Languages (COORDINATION) (Lecture Notes in Computer Science, Vol. 10852). Springer, 252–279. https://doi.org/10.1007/978-3-319-92408-3_12

Digital Library

Cited By

Audrito GDamiani FTorta GAncona DAudrito G(2024)Real-Time Guarantees for SLCS Monitors in XCProceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution10.1145/3679008.3685545(32-37)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679008.3685545

Index Terms

Optimising Aggregate Monitors for Spatial Logic of Closure Spaces Properties
1. Computing methodologies
  1. Distributed computing methodologies
    1. Distributed programming languages
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Towards aggregate monitoring of spatio-temporal properties
VORTEX 2021: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution

As the cost of computing devices continues to decrease, swarms of low-end intelligent devices become a more interesting solution for safety-critical applications. The safe execution of such systems, however, usually requires mechanisms ensuring that ...
Combining Static and Runtime Verification with AC and Coq
VORTEX 2023: Proceedings of the 6th International Workshop on Verification and Monitoring at Runtime Execution

The 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 ...
Synthesising correct concurrent runtime monitors

This paper studies the correctness of automated synthesis for concurrent monitors. We adapt a subset of the Hennessy---Milner logic with recursion (a reformulation of the modal $$\mu $$μ-calculus) to specify safety properties for Erlang programs. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

VORTEX 2024: Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution

September 2024

51 pages

ISBN:9798400711190

DOI:10.1145/3679008

General Chairs:
Davide Ancona
University of Genova, Italy
,
Giorgio Audrito
Università di Torino, Italy

Copyright © 2024 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 September 2024

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Ministero dell'Università e della Ricerca
Ministero dell'Università e della Ricerca

Conference

VORTEX '24

Sponsor:

SIGSOFT

VORTEX '24: 7th ACM International Workshop on Verification and Monitoring at Runtime Execution

September 19, 2024

Vienna, Austria

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
51
Total Downloads

Downloads (Last 12 months)51
Downloads (Last 6 weeks)14

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Audrito GDamiani FTorta GAncona DAudrito G(2024)Real-Time Guarantees for SLCS Monitors in XCProceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution10.1145/3679008.3685545(32-37)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679008.3685545

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents