Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/3679008.3685545acmconferencesArticle/Chapter ViewAbstractPublication PagesisstaConference Proceedingsconference-collections
research-article
Open access

Real-Time Guarantees for SLCS Monitors in XC

Published: 13 September 2024 Publication History

Abstract

The behavior of distributed systems situated in space can be required to satisfy spatial properties, in addition to the more widely known temporal properties. In particular, it has been previously shown that fully distributed monitors in eXchange Calculus (XC) can be automatically derived for verifying properties of situated systems expressed in the Spatial Logic of Closure Spaces (SLCS). While it has been proven that such monitors eventually compute the truth value of the desired properties, the actual time required for such computations has been thus far disregarded. In the present paper, we fill this gap by investigating the real-time guarantees that can be given in terms of upper bounds on the time taken by the XC monitors to compute the truth of SLCS properties after stabilisation of inputs.

References

[1]
Gianluca Aguzzi, Giorgio Audrito, and Mirko Viroli. 2024. Optimising Aggregate Monitors for Spatial Logic of Closure Spaces Properties. In VORTEX 2024: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution. ACM. https://doi.org/10.1145/3679008.3685544
[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
[4]
Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Guido Salvaneschi, and Mirko Viroli. 2022. Functional Programming for Distributed Systems with XC. In 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany, Karim Ali and Jan Vitek (Eds.) (LIPIcs, Vol. 222). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 20:1–20:28. https://doi.org/10.4230/LIPICS.ECOOP.2022.20
[5]
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
[6]
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
[7]
Giorgio Audrito, Roberto Casadei, and Gianluca Torta. 2021. Towards Integration of Multi-Agent Planning with Self-Organising Collective Processes. In IEEE International Conference on Autonomic Computing and Self-Organizing Systems, ACSOS 2021, Companion Volume, Washington, DC, USA, September 27 - Oct. 1, 2021, Esam El-Araby, Vana Kalogeraki, Danilo Pianini, Frédéric Lassabe, Barry Porter, Sona Ghahremani, Ingrid Nunes, Mohamed Bakhouya, and Sven Tomforde (Eds.). IEEE, 297–298. https://doi.org/10.1109/ACSOS-C52956.2021.00042
[8]
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
[9]
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
[10]
Giorgio Audrito, Ferruccio Damiani, and Gianluca Torta. 2024. Towards Real-Time Aggregate Computing. 12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2024). To appear
[11]
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
[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
[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. https://doi.org/10.1109/MC.2015.261
[15]
Roberto Casadei, Gianluca Aguzzi, Danilo Pianini, and Mirko Viroli. 2023. Programming (and Learning) Self-Adaptive & Self-Organising Behaviour with ScaFi: for Swarms, Edge-Cloud Ecosystems, and More. In IEEE International Conference on Autonomic Computing and Self-Organizing Systems, ACSOS 2023 - Companion, Toronto, ON, Canada, September 25-29, 2023. IEEE, 33–34. https://doi.org/10.1109/ACSOS-C58168.2023.00032
[16]
Roberto Casadei and Mirko Viroli. 2016. Towards Aggregate Programming in Scala. In First Workshop on Programming Models and Languages for Distributed Computing (PMLDC ’16). ACM, Article 5, 5:1–5:7 pages. isbn:978-1-4503-4775-4 https://doi.org/10.1145/2957319.2957372
[17]
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
[18]
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) (Lecture Notes in Computer Science, Vol. 8705). Springer, 222–235. https://doi.org/10.1007/978-3-662-44602-7_18
[19]
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
[20]
Yogi Joshi, Guy Martin Tchamgoue, and Sebastian Fischmeister. 2017. Runtime verification of LTL on lossy traces. In Proceedings of the Symposium on Applied Computing (SAC ’17). Association for Computing Machinery, New York, NY, USA. 1379–1386. isbn:9781450344869 https://doi.org/10.1145/3019612.3019827
[21]
Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 21, 7 (1978), 558–565.
[22]
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
[23]
Menna Mostafa and Borzoo Bonakdarpour. 2015. Decentralized Runtime Verification of LTL Specifications in Distributed Systems. In 2015 IEEE International Parallel and Distributed Processing Symposium. 494–503. https://doi.org/10.1109/IPDPS.2015.95
[24]
Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink. 2018. Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL. Log. Methods Comput. Sci., 14, 4 (2018), https://doi.org/10.23638/LMCS-14(4:2)2018
[25]
Tommy Tracy, Lucas M. Tabajara, Moshe Vardi, and Kevin Skadron. 2020. Runtime Verification on FPGAs with LTLf Specifications. In 2020 Formal Methods in Computer Aided Design (FMCAD). 36–46. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_10
[26]
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

Cited By

View all
  • (2024)Optimising Aggregate Monitors for Spatial Logic of Closure Spaces PropertiesProceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution10.1145/3679008.3685544(25-31)Online publication date: 13-Sep-2024

Recommendations

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
This work is licensed under a Creative Commons Attribution-ShareAlike 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.

Check for updates

Author Tags

  1. aggregate computing
  2. real-time
  3. runtime verification
  4. spatial logic

Qualifiers

  • Research-article

Conference

VORTEX '24
Sponsor:

Upcoming Conference

ISSTA '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)47
  • Downloads (Last 6 weeks)11
Reflects downloads up to 24 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Optimising Aggregate Monitors for Spatial Logic of Closure Spaces PropertiesProceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution10.1145/3679008.3685544(25-31)Online publication date: 13-Sep-2024

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media