Abstract
We consider monitoring and checking formally specified properties in a network. We are addressing the problem of deploying the checkers on different network nodes that provide correct and efficient checking. We present the DMaC system that builds upon two bodies of work: the Monitoring and Checking (MaC) framework, which provides means to monitor and check running systems against formally specified requirements, and declarative networking, a declarative domain-specific approach for specifying and implementing distributed network protocols. DMaC uses a declarative networking system for both specifying network protocols and performing checker execution. High-level properties are automatically translated from safety property specifications in the MaC framework into declarative networking queries and integrated into the rest of the network for monitoring the safety properties. We evaluate the flexibility and efficiency of DMaC using simple but realistic network protocols and their properties.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
P2: Declarative Networking, http://p2.cs.berkeley.edu
Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006)
Chen, F., Rosu, G.: MOP: An efficient and generic runtime verification framework. In: Proceedings of OOPSLA 2007, pp. 569–588 (2007)
Colombo, C., Pace, G., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008) (September 2008)
Deshpande, A., Ives, Z.G., Raman, V.: Adaptive query processing. Foundations and Trends in Databases 1(1), 1–140 (2007)
Diaz, M., Juanole, G., Courtiat, J.-P.: Observer - a concept for formal on-line validation of distributed systems. IEEE Transactions on Software Engineering 20(12), 900–913 (1994)
Havelund, K., Rosu, G.: Monitoring Java programs with JavaPathExplorer. In: Proceedings of the Workshop on Runtime Verification. Electronic Notes in Theoretical Computer Science, vol. 55. Elsevier Publishing, Amsterdam (2001)
Herbert, D., Sundaram, V., Lu, Y.-H., Bagchi, S., Li, Z.: Adaptive correctness monitoring for wireless sensor networks using hierarchical distributed run-time invariant checking. ACM Transactions on Autonomous and Adaptive Systems 2(3) (2007)
Jahanian, F., Goyal, A.: A formalism for monitoring real-time constraints at run-time. In: 20th Int. Symp. on Fault-Tolerant Computing Systems (FTCS-20), pp. 148–155 (1990)
Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: a run-time assurance approach for Java programs. Formal Methods in Systems Design 24(2), 129–155 (2004)
Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: Formally specified monitoring of temporal properties. In: Proceedings of the European Conf. on Real-Time Systems - ECRTS 1999, June 1999, pp. 114–121 (1999)
Liu, X., Guo, Z., Wang, X., Chen, F., Tang, X.L.J., Wu, M., Kaashoek, M.F., Zhang, Z.: D3S: Debugging Deployed Distributed Systems. In: NSDI (2008)
Loo, B.T., Condie, T., Hellerstein, J.M., Maniatis, P., Roscoe, T., Stoica, I.: Implementing Declarative Overlays. In: ACM SOSP (2005)
Loo, B.T., Hellerstein, J.M., Stoica, I., Ramakrishnan, R.: Declarative Routing: Extensible Routing with Declarative Queries. In: SIGCOMM (2005)
Mok, A.K., Liu, G.: Efficient run-time monitoring of timing constraints. In: IEEE Real-Time Technology and Applications Symposium (June 1997)
Paxson, V., Kurose, J., Partridge, C., Zegura, E.W.: End-to-end routing behavior in the internet. IEEE/ACM Transactions on Networking, 601–615 (1996)
Reynolds, P., Killian, C., Wiener, J.L., Mogul, J.C., Shah, M.A., Vahdat, A.: Pip: Detecting the Unexpected in Distributed Systems. In: NSDI (2006)
Sankar, S., Mandal, M.: Concurrent runtime monitoring of formally specified programs. IEEE Computer (1993)
Savor, T., Seviora, R.E.: Toward automatic detection of software failures. IEEE Computer, 68–74 (August 1998)
Selinger, P.G., Astrahan, M.M., Chamberlin, D.D., Lorie, R.A., Price, T.G.: Access path selection in a relational database management system. In: SIGMOD (1979)
Sen, K., Rosu, G., Agha, G.: Online efficient predictive safety analysis of multithreaded programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 123–138. Springer, Heidelberg (2004)
Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: 26th International Conference on Software Engineering (ICSE 2004), pp. 418–427 (2004)
Sokolsky, O., Sammapun, U., Lee, I., Kim, J.: Run-time checking of dynamic properties. In: Proceeding of the 5th International Workshop on Runtime Verification (RV 2005), Edinburgh, Scotland, UK (July 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhou, W., Sokolsky, O., Loo, B.T., Lee, I. (2009). DMaC: Distributed Monitoring and Checking. In: Bensalem, S., Peled, D.A. (eds) Runtime Verification. RV 2009. Lecture Notes in Computer Science, vol 5779. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04694-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-04694-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04693-3
Online ISBN: 978-3-642-04694-0
eBook Packages: Computer ScienceComputer Science (R0)