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
Tax calculation will be finalised at checkout
Purchases are for personal use only
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
Corresponding author
Editor information
Editors and Affiliations
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
DOI: https://doi.org/10.1007/978-3-319-67531-2_20
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)