Part of the book series:Lecture Notes in Computer Science ((LNPSE,volume 10548))
Included in the following conference series:
Abstract
Run-time checking of timed properties requires to monitor events occurring within a specified time interval. In a distributed setting, working with intervals is complicated due to uncertainties about network delays and clock synchronization. Determining that an interval can be closed – i.e., that all events occurring within the interval have been observed – cannot be done without a delay. In this paper, we consider how an appropriate delay can be determined based on parameters of a monitoring setup, such as network delay, clock skew and clock rate. We then propose a generic scheme for monitoring time intervals, parameterized by the detection delay, and discuss the use of this monitoring scheme to check different timed specifications, including real-time temporal logics and rate calculations.
This work is supported in part by DARPA BRASS program under contract FA8750-16-C-0007 and by ONR SBIR contract N00014-15-C-0126.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Sammapun, U.: Monitoring and checking of real-time and probabilistic properties. Ph.D. thesis, University of Pennsylvania (2009)
Lee, I., Davidson, S.B.: Adding time to synchronous process communications. IEEE Trans. Comput.100(8), 941–948 (1987)
Lee, I., Davidson, S.B.: A performance analysis of timed synchronous communication primitives. IEEE Trans. Comput.39(9), 1117–1131 (1990)
Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H., Rollet, A., Timo, O.N.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des.45(3), 381–422 (2014)
Jahanian, F., Rajkumar, R., Raju, S.C.: Runtime monitoring of timing constraints in distributed real-time systems. Real-Time Syst.7(3), 247–273 (1994)
Finkbeiner, B., Sankaranarayanan, S., Sipma, H.B.: Collecting statistics over runtime executions. Formal Methods Syst. Des.27(3), 253–274 (2005)
Colombo, C., Gauci, A., Pace, G.J.: LarvaStat: Monitoring of statistical properties. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 480–484. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_38
Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 40–58. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40787-1_3
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, Cham (2014). doi:10.1007/978-3-319-11164-3_16
Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: a run-time assurance approach for Java programs. Formal Methods Syst. Des.24(2), 129–155 (2004)
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Logic Comput.20(3), 675–706 (2010)
Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng.12(2), 151–197 (2005)
Leland, W.E., Taqqu, M.S., Willinger, W., Wilson, D.V.: On the self-similar nature of ethernet traffic. In: ACM SIGCOMM Computer Communication Review, vol. 23, pp. 183–193. ACM (1993)
Becchi, M.: From poisson processes to self-similarity: a survey of network traffic models. Washington University in St. Louis, Technical Report (2008)
Author information
Authors and Affiliations
University of Pennsylvania, Philadelphia, PA, USA
Teng Zhang, Insup Lee & Oleg Sokolsky
BAE Systems, Burlington, MA, USA
John Wiegley
- Teng Zhang
You can also search for this author inPubMed Google Scholar
- John Wiegley
You can also search for this author inPubMed Google Scholar
- Insup Lee
You can also search for this author inPubMed Google Scholar
- Oleg Sokolsky
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toTeng Zhang.
Editor information
Editors and Affiliations
Microsoft Research, Redmond, Washington, USA
Shuvendu Lahiri
The University of Manchester, Manchester, United Kingdom
Giles Reger
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Zhang, T., Wiegley, J., Lee, I., Sokolsky, O. (2017). Monitoring Time Intervals. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_20
Download citation
Published:
Publisher Name:Springer, Cham
Print ISBN:978-3-319-67530-5
Online ISBN:978-3-319-67531-2
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative