Abstract
Runtime verification can effectively increase the reliability of software systems. In recent years, parametric runtime verification has gained a lot of traction, with several systems proposed. However, lack of real specifications and prohibitive runtime overhead when checking numerous properties simultaneously prevent developers or users from using runtime verification. This paper reports on more than 150 formal specifications manually derived from the Java API documentation of commonly used packages, as well as a series of novel techniques which resulted in a new runtime verification system, RV-Monitor. Experiments show that these specifications are useful for finding bugs and bad software practice, and RV-Monitor is capable of monitoring all our specifications simultaneously, and runs substantially faster than other state-of-the-art runtime verification systems.
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
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA (2005)
Ammons, G., Bodík, R., Larus, J.R.: Mining specifications. In: POPL (2002)
Annotated Java API Specifications, https://code.google.com/p/annotated-java-api/
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from EAGLE to RULER. J. Logic Computation (November 2008)
Blackburn, S.M., Garner, R., Hoffman, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M., Lee, H., Moss, J.E.B., Phansalkar, A., Stefanović, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA (2006)
Bodden, E.: J-LO, a tool for runtime-checking temporal assertions. Master’s thesis, RWTH Aachen University (2005)
Chaudhuri, S., Alur, R.: Instrumenting C programs with nested word monitors. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 279–283. Springer, Heidelberg (2007)
Chen, F., Meredith, P., Jin, D., Rosu, G.: Efficient formalism-independent monitoring of parametric properties. In: ASE (2009)
d’Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. SIGSOFT Softw. Eng. Notes (2005)
Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)
Ernst, M.D., Czeisler, A., Griswold, W.G., Notkin, D.: Quickly detecting relevant program invariants. In: ICSE (2000)
Gabel, M., Su, Z.: Symbolic mining of temporal specifications. In: ICSE (2008)
Goldsmith, S., O’Callahan, R., Aiken, A.: Relational queries over program traces. In: OOPSLA (2005)
Havelund, K., Roşu, G.: Monitoring Java programs with Java PathExplorer. In: RV (2001)
Jin, D., Meredith, P.O., Griffith, D., Roşu, G.: Garbage collection for monitoring parametric properties. In: PLDI (2011)
Jin, D., Meredith, P.O., Roşu, G.: Scalable parametric runtime monitoring. Technical Report, Department of Computer Science, University of Illinois at Urbana-Champaign (2012), http://hdl.handle.net/2142/30757
Lee, C., Chen, F., Roşu, G.: Mining parametric specifications. In: ICSE (2011)
Lee, C., Jin, D., Meredith, P.O., Roşu, G.: Towards categorizing and formalizing the JDK API. Technical Report, Department of Computer Science, University of Illinois at Urbana-Champaign (2012), http://hdl.handle.net/2142/30006
Martin, M., Livshits, V.B., Lam, M.S.: Finding application errors and security flaws using PQL: a program query language. In: OOPSLA. ACM (2005)
Meredith, P.O., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the MOP runtime verification framework. STTT (2011)
Purandare, R., Dwyer, M.B., Elbaum, S.G.: Optimizing monitoring of finite state properties through monitor compaction. In: ISSTA (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Luo, Q. et al. (2014). RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties. In: Bonakdarpour, B., Smolka, S.A. (eds) Runtime Verification. RV 2014. Lecture Notes in Computer Science, vol 8734. Springer, Cham. https://doi.org/10.1007/978-3-319-11164-3_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-11164-3_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11163-6
Online ISBN: 978-3-319-11164-3
eBook Packages: Computer ScienceComputer Science (R0)