More Web Proxy on the site http://driver.im/

research-article

Monitoring decentralized specifications

Authors:

Antoine El-Hokayem,

Yliès FalconeAuthors Info & Claims

ISSTA 2017: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis

Pages 125 - 135

https://doi.org/10.1145/3092703.3092723

Published: 10 July 2017 Publication History

Abstract

We define two complementary approaches to monitor decentralized systems. The first relies on those with a centralized specification, i.e, when the specification is written for the behavior of the entire system. To do so, our approach introduces a data-structure that i) keeps track of the execution of an automaton, ii) has predictable parameters and size, and iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study decentralized monitorability, and present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Lastly, we introduce our tool, which is a framework for designing such decentralized algorithms, and simulating their behavior.

Supplementary Material

Auxiliary Archive (issta17-mainid83-s.zip)

# THEMIS - A Tool for Decentralized Monitoring Algorithms The artifact repository for the [ISSTA 2017](http://conf.researchr.org/home/issta-2017) paper: *Monitoring Decentralized Specifications*. ## Reading the README.md Files ## All README.md files are pre-rendered as HTML for convenience. In each directory (including this one), the 'index.html' file corresponds to a rendered 'README.md'. ## Related Papers * Antoine El-Hokayem and Ylies Falcone. 2017. Monitoring Decentralized Specifications. In Proceedings of the 26th International Symposium on Softare Testing and Analysis, ISSTA 2017, Santa-Barbara, USA, July 10-14, 2017.

Download
256.84 MB

References

[1]

Ezio Bartocci. 2013. Sampling-based Decentralized Monitoring for Networked Embedded Systems. In Proceedings Third International Workshop on Hybrid Autonomous Systems, HAS 2013, Rome, Italy, 17th March 2013. (EPTCS), Luca Bortolussi, Manuela L. Bujorianu, and Giordano Pola (Eds.), Vol. 124. 85–99.

[2]

Ezio Bartocci, Yliès Falcone, Borzoo Bonakdarpour, Christian Colombo, Normann Decker, Klaus Havelund, Yogi Joshi, Felix Klaedtke, Reed Milewicz, Giles Reger, Grigore Rosu, Julien Signoles, Daniel Thoma, Eugen Zalinescu, and Yi Zhang. 2017. First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. International Journal on Software Tools for Technology Transfer (2017), 1–40.

[3]

David A. Basin, Felix Klaedtke, and Eugen Zalinescu. 2015. Failure-aware Runtime Verification of Distributed Systems. In 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India (LIPIcs), Prahladh Harsha and G. Ramalingam (Eds.), Vol. 45. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 590–603.

[4]

Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20, 4 (2011), 14.

Digital Library

[5]

Andreas Klaus Bauer and Yliès Falcone. 2012. Decentralised LTL Monitoring. In FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27- 31, 2012. Proceedings (Lecture Notes in Computer Science), Dimitra Giannakopoulou and Dominique Méry (Eds.), Vol. 7436. Springer, 85–100.

[6]

Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, and Corentin Travers. 2016. Challenges in Fault-Tolerant Distributed Runtime Verification, See {23}, 363–370.

[7]

David Buchfuhrer and Christopher Umans. 2008. The Complexity of Boolean Formula Minimization. In Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games (Lecture Notes in Computer Science), Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz (Eds.), Vol. 5125. Springer, 24–35.

Digital Library

[8]

Christian Colombo and Yliès Falcone. 2016. Organising LTL monitors over distributed systems with a global clock. Formal Methods in System Design 49, 1-2 (2016), 109–158.

Digital Library

[9]

Sylvain Cotard, Sébastien Faucou, Jean-Luc Béchennec, Audrey Queudet, and Yvon Trinquet. 2012. A Data Flow Monitoring Service Based on Runtime Verification for AUTOSAR. In 14th IEEE International Conference on High Performance Computing and Communication & 9th IEEE International Conference on Embedded Software and Systems, HPCC-ICESS 2012, Liverpool, United Kingdom, June 25-27, 2012, Geyong Min, Jia Hu, Lei (Chris) Liu, Laurence Tianruo Yang, Seetharami Seelam, and Laurent Lefèvre (Eds.). IEEE Computer Society, 1508–1515.

Digital Library

[10]

Volker Diekert and Martin Leucker. 2014. Topology, monitorable properties and runtime verification. Theoretical Computer Science 537 (2014), 29 – 41.

[11]

Volker Diekert and Anca Muscholl. 2012. On Distributed Monitoring of Asynchronous Systems. In Logic, Language, Information and Computation - 19th International Workshop, WoLLIC 2012, Buenos Aires, Argentina, September 3-6, 2012. Proceedings (Lecture Notes in Computer Science), C.-H. Luke Ong and Ruy J. G. B. de Queiroz (Eds.), Vol. 7456. Springer, 70–84.

[12]

Alexandre Duret-Lutz. 2013. Manipulating LTL formulas using Spot 1.0. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13) (Lecture Notes in Computer Science), Vol. 8172. Springer, Hanoi, Vietnam, 442–445.

[13]

Antoine El-Hokayem and Yliès Falcone. 2017. THEMIS: A Tool for Decentralized Monitoring Algorithms. In Proceedings of 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’17-DEMOS), Santa Barbara, CA, USA, July 2017.

Digital Library

[14]

Antoine El-Hokayem and Yliès Falcone. 2017. THEMIS Website. (2017). https: //gitlab.inria.fr/monitoring/themis.

[15]

Yliès Falcone. 2010. You Should Better Enforce Than Verify. In Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings (Lecture Notes in Computer Science), Howard Barringer, Yliès Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon J. Pace, Grigore Rosu, Oleg Sokolsky, and Nikolai Tillmann (Eds.), Vol. 6418. Springer, 89–105.

Digital Library

[16]

Yliès Falcone, Tom Cornebize, and Jean-Claude Fernandez. 2014. Efficient and Generalized Decentralized Monitoring of Regular Languages. In Formal Techniques for Distributed Objects, Components, and Systems - 34th IFIP WG 6.1 International Conference, FORTE 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014. Proceedings (Lecture Notes in Computer Science), Erika Ábrahám and Catuscia Palamidessi (Eds.), Vol. 8461. Springer, 66–83.

[17]

Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. 2012. What can you verify and enforce at runtime? STTT 14, 3 (2012), 349–382. //dx.

[18]

Yliès Falcone, Klaus Havelund, and Giles Reger. 2013. A Tutorial on Runtime Verification. In Engineering Dependable Software Systems, Manfred Broy, Doron a. Peled, and Georg Kalus (Eds.). NATO science for peace and security series, d: information and communication security, Vol. 34. ios press, 141–175.

[19]

Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm, and William G. Griswold. 2001. An Overview of AspectJ. In ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary, June 18-22, 2001, Proceedings (Lecture Notes in Computer Science), Jørgen Lindskov Knudsen (Ed.), Vol. 2072. Springer, 327–353.

Digital Library

[20]

Moonjoo Kim, Mahesh Viswanathan, Hanêne Ben-Abdallah, Sampath Kannan, Insup Lee, and Oleg Sokolsky. 1999. Formally specified monitoring of temporal properties. In 11th Euromicro Conference on Real-Time Systems (ECRTS 1999), 9-11 June 1999, York, England, UK, Proceedings. IEEE Computer Society, 114–122.

[21]

Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification. J. Log. Algebr. Program. 78, 5 (2009), 293–303.

[22]

Martin Leucker, Malte Schmitz, and Danilo à Tellinghusen. 2016. Runtime Verification for Interconnected Medical Devices, See {23}, 380–387. //dx.

[23]

Tiziana Margaria and Bernhard Steffen (Eds.). 2016. Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. Lecture Notes in Computer Science, Vol. 9953.

[24]

Amir Pnueli and Aleksandr Zaks. 2006. PSL Model Checking and Run-Time Verification Via Testers. In FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings (Lecture Notes in Computer Science), Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (Eds.), Vol. 4085. Springer, 573–586.

Digital Library

[25]

Grigore Rosu and Klaus Havelund. 2005. Rewriting-Based Techniques for Runtime Verification. Autom. Softw. Eng. 12, 2 (2005), 151–197. //dx.

Digital Library

[26]

Torben Scheffel and Malte Schmitz. 2014. Three-valued asynchronous distributed runtime verification. In Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2014, Lausanne, Switzerland, October 19-21, 2014. IEEE, 52–61.

Digital Library

[27]

6961843

[28]

Koushik Sen, Abhay Vardhan, Gul Agha, and Grigore Rosu. 2004. Efficient Decentralized Monitoring of Safety in Distributed Systems. In 26th International Conference on Software Engineering (ICSE 2004), 23-28 May 2004, Edinburgh, United Kingdom, Anthony Finkelstein, Jacky Estublier, and David S. Rosenblum (Eds.). IEEE Computer Society, 418–427.

Digital Library

[29]

Marc Shapiro, Nuno M. Preguiça, Carlos Baquero, and Marek Zawirski. 2011. Conflict-Free Replicated Data Types. In Stabilization, Safety, and Security of Distributed Systems - 13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011. Proceedings (Lecture Notes in Computer Science), Xavier Défago, Franck Petit, and Vincent Villain (Eds.), Vol. 6976. Springer, 386–400.

Digital Library

[30]

Prasanna Thati and Grigore RoÅ§u. 2005. Monitoring Algorithms for Metric Temporal Logic Specifications. Electronic Notes in Theoretical Computer Science 113 (2005), 145 – 162.

[31]

Leslie G. Valiant. 1990. A Bridging Model for Parallel Computation. Commun. ACM 33, 8 (Aug. 1990), 103–111.

Digital Library

Cited By

Mahe EBannour BGaston CLe Gall P(2024)Efficient Interaction-Based Offline Runtime Verification of Distributed Systems with Lifeline RemovalScience of Computer Programming10.1016/j.scico.2024.103230(103230)Online publication date: Nov-2024
https://doi.org/10.1016/j.scico.2024.103230
Danielsson LSánchez C(2023)Decentralized Stream Runtime Verification for Timed Asynchronous NetworksIEEE Access10.1109/ACCESS.2023.329832911(84091-84112)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3298329
Gallay FFalcone Y(2022)Decent: A Benchmark for Decentralized EnforcementRuntime Verification10.1007/978-3-031-17196-3_18(293-303)Online publication date: 28-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17196-3_18
Show More Cited By

Index Terms

Monitoring decentralized specifications
1. Computing methodologies
  1. Concurrent computing methodologies
    1. Concurrent algorithms
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation

We introduce two complementary approaches to monitor decentralized systems. The first approach relies on systems with a centralized specification, i.e., when the specification is written for the behavior of the entire system. To do so, our approach ...
Bringing runtime verification home: a case study on the hierarchical monitoring of smart homes using decentralized specifications
Abstract
We use runtime verification (RV) to check various specifications in a smart apartment. The specifications can be broken down into three types: behavioral correctness of the apartment sensors, detection of specific user activities (known as ...
Operational and Declarative Runtime Verification (Keynote)
VORTEX 2024: Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution

Runtime verification (RV) is used to monitor executions of a system, checking them against a formal specification. It can detect failures, and can also be used to control a system, diverting its operation to avoid a failure. One can identify two main ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA 2017: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis

July 2017

447 pages

ISBN:9781450350761

DOI:10.1145/3092703

General Chair:
Tevfik Bultan
University of California at Santa Barbara, USA
,
Program Chair:
Koushik Sen
University of California at Berkeley, USA

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part 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 components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 July 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

ISSTA '17

Sponsor:

SIGSOFT

ISSTA '17: International Symposium on Software Testing and Analysis

July 10 - 14, 2017

CA, Santa Barbara, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

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

16
Total Citations
View Citations
182
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)1

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mahe EBannour BGaston CLe Gall P(2024)Efficient Interaction-Based Offline Runtime Verification of Distributed Systems with Lifeline RemovalScience of Computer Programming10.1016/j.scico.2024.103230(103230)Online publication date: Nov-2024
https://doi.org/10.1016/j.scico.2024.103230
Danielsson LSánchez C(2023)Decentralized Stream Runtime Verification for Timed Asynchronous NetworksIEEE Access10.1109/ACCESS.2023.329832911(84091-84112)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3298329
Gallay FFalcone Y(2022)Decent: A Benchmark for Decentralized EnforcementRuntime Verification10.1007/978-3-031-17196-3_18(293-303)Online publication date: 28-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17196-3_18
Gallay FFalcone Y(2021)Decentralized LTL EnforcementElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.346.9346(135-151)Online publication date: 17-Sep-2021
https://doi.org/10.4204/EPTCS.346.9
El-Hokayem AFalcone Y(2020)On the Monitoring of Decentralized SpecificationsACM Transactions on Software Engineering and Methodology10.1145/335518129:1(1-57)Online publication date: 30-Jan-2020
https://dl.acm.org/doi/10.1145/3355181
Betti QMontreuil BKhoury RHallé S(2020)Smart Contracts-Enabled Simulation for Hyperconnected LogisticsDecentralised Internet of Things10.1007/978-3-030-38677-1_6(109-149)Online publication date: 13-Feb-2020
https://doi.org/10.1007/978-3-030-38677-1_6
Bataineh ORosenblum DReynolds M(2019)Efficient Decentralized LTL Monitoring Framework Using Tableau TechniqueACM Transactions on Embedded Computing Systems10.1145/335821918:5s(1-21)Online publication date: 11-Oct-2019
https://dl.acm.org/doi/10.1145/3358219
Bur MVarro D(2019)Evaluation of Distributed Query-Based Monitoring over Data Distribution Service2019 IEEE 5th World Forum on Internet of Things (WF-IoT)10.1109/WF-IoT.2019.8767281(674-679)Online publication date: Apr-2019
https://doi.org/10.1109/WF-IoT.2019.8767281
Sánchez CSchneider GAhrendt WBartocci EBianculli DColombo CFalcone YFrancalanza AKrstić SLourenço JNickovic DPace GRufino JSignoles JTraytel DWeiss A(2019)A survey of challenges for runtime verification from advanced application domains (beyond software)Formal Methods in System Design10.1007/s10703-019-00337-w54:3(279-335)Online publication date: 11-Nov-2019
https://doi.org/10.1007/s10703-019-00337-w
Kühn eRadschek SElaraby N(2018)Distributed Coordination Runtime Assertions for the Peer ModelCoordination Models and Languages10.1007/978-3-319-92408-3_9(200-219)Online publication date: 27-May-2018
https://doi.org/10.1007/978-3-319-92408-3_9
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents