Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Some Thoughts on Runtime Verification Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Precision, Recall, and Sensitivity of Monitoring Partially Synchronous Distributed Systems

Authors : Sorrachai Yingchareonthawornchai, Duong N. Nguyen, Vidhya Tekken Valapil, Sandeep S. Kulkarni, Murat Demirbas

Published in: Runtime Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Runtime verification focuses on analyzing the execution of a given program by a monitor to determine if it is likely to violate its specifications. There is often an impedance mismatch between the assumptions/model of the monitor and that of the underlying program. This constitutes problems especially for distributed systems, where the concept of current time and state are inherently uncertain. A monitor designed with asynchronous system model assumptions may cause false-positives for a program executing in a partially synchronous system: the monitor may flag a global predicate that does not actually occur in the underlying system. A monitor designed with a partially synchronous system model assumption may cause false negatives as well as false positives for a program executing in an environment where the bounds on partial synchrony differ (albeit temporarily) from the monitor model assumptions.
In this paper we analyze the effects of the impedance mismatch between the monitor and the underlying program for the detection of conjunctive predicates. We find that there is a small interval where the monitor assumptions are hypersensitive to the underlying program environment. We provide analytical derivations for this interval, and also provide simulation support for exploring the sensitivity of predicate detection to the impedance mismatch between the monitor and the program under a partially synchronous system.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Decision-Theoretic Monitoring of Cyber-Physical Systems
next chapter Falsification of Conditional Safety Properties for Cyber-Physical Systems with Gaussian Process Regression
Footnotes
1
Following Lamport’s definition of causality [5], for any two events e and f, we say that \(e hb \) f (e happened before f) if and only if (1) e and f are events in the same process and e occurred before f, (2) e is a send event and f is the corresponding receive event, or (3) there exists an event g such that \(e hb \) g and \(g hb \) f.
 
2
As validated in Sect. 3, the value of \(\delta \) is not important. Hence, we only focus on the relation between \(\epsilon _{mon}\) and \(\epsilon _{app}\).
 
Literature
1.
Fan, R., Lynch, N.: Gradient clock synchronization. In: PODC, pp. 320–327 (2004)
2.
Patt-Shamir, B., Rajsbaum, S.: A theory of clock synchronization (extended abstract). In: ACM Symposium on Theory of Computing (STOC), pp. 810–819 (1994)
3.
4.
Mills, D.: A brief history of NTP time: memoirs of an internet timekeeper. ACM SIGCOMM Comput. Commun. Rev. 33(2), 9–21 (2003)CrossRef
5.
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefMATH
6.
Yingchareonthawornchai, S., Nguyen, D., Valapil, V.T., Kulkarni, S.S., Demirbas, M.: Precision, recall, sensitivity of monitoring partially synchronous distributed systems. CoRR, abs/1607.03369 (2016). http://​arxiv.​org/​abs/​1607.​03369
7.
Garg, V.K., Chase, C.: Distributed algorithms for detecting conjunctive predicates. In: International Conference on Distributed Computing Systems, pp. 423–430, June 1995
8.
Lu, H., Veeraraghavan, K., Ajoux, P., Hunt, J., Song, Y.-J., Tobagus, W., Kumar, S., Lloyd, W.: Existential consistency: measuring and understanding consistency at Facebook. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 295–310. ACM (2015)
9.
10.
Chow, M., Meisner, D., Flinn, J., Peek, D., Wenisch, T.: The mystery machine: end-to-end performance analysis of large-scale internet services. In: 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2014), pp. 217–231 (2014)
11.
Cooper, R., Marzullo, K.: Consistent detection of global predicates. ACM SIGPLAN Not. 26(12), 167–174 (1991)CrossRef
12.
Verissimo, P.: Real-time communication. In: Distributed Systems, vol. 2 (1993)
13.
Stoller, S.: Detecting global predicates in distributed systems with clocks. Distrib. Comput. 13(2), 85–98 (2000)CrossRef
14.
Kulkarni, S.S., Demirbas, M., Madappa, D., Avva, B., Leone, M.: Logical physical clocks. In: Aguilera, M.K., Querzoni, L., Shapiro, M. (eds.) OPODIS 2014. LNCS, vol. 8878, pp. 17–32. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-14472-6_​2
15.
Demirbas, M., Kulkarni, S.: Beyond truetime: using augmentedtime for improving google spanner. In: 7th Workshop on Large-Scale Distributed Systems and Middleware, LADIS (2013)
16.
17.
Yingchareonthawornchai, S., Kulkarni, S., Demirbas, M.: Analysis of bounds on hybrid vector clocks. In: 19th International Conference on Principles of Distributed Systems, OPODIS (2015)
18.
19.
Wang, S., Ayoub, A., Sokolsky, O., Lee, I.: Runtime verification of traces under recording uncertainty. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 442–456. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-29860-8_​35 CrossRef
20.
Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 2015 IEEE International Parallel, Distributed Processing Symposium, IPDPS 2015, 25–29 May 2015 Hyderabad, India, pp. 494–503 (2015). http://​dx.​doi.​org/​10.​1109/​IPDPS.​2015.​95
21.
Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: On real-time monitoring with imprecise timestamps. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 193–198. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-11164-3_​16
Metadata
Title
Precision, Recall, and Sensitivity of Monitoring Partially Synchronous Distributed Systems
Authors
Sorrachai Yingchareonthawornchai
Duong N. Nguyen
Vidhya Tekken Valapil
Sandeep S. Kulkarni
Murat Demirbas
Copyright Year
2016
Book
Runtime Verification

Print ISBN: 978-3-319-46981-2

Electronic ISBN: 978-3-319-46982-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-46982-9_26

Premium Partner

    Image Credits