Abstract
Clara is a novel static-analysis framework for partially evaluating finite-state runtime monitors at compile time. Clara uses static typestate analyses to automatically convert any AspectJ monitoring aspect into a residual runtime monitor that only monitors events triggered by program locations that the analyses failed to prove safe. If the static analysis succeeds on all locations, this gives strong static guarantees. If not, the efficient residual runtime monitor is guaranteed to capture property violations at runtime. Researchers can use Clara with most runtime-monitoring tools that implement monitors as AspectJ aspects.
In this tutorial supplement, we provide references to related reading material that will allow the reader to obtain in-depth knowledge about the context in which Clara can be applied and about the techniques that underlie the Clara framework.
This work was supported by CASED (www.cased.de).
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding Trace Matching with Free Variables to AspectJ. In: OOPSLA, pp. 345–364 (October 2005)
Ammons, G., Bodík, R., Larus, J.R.: Mining specifications. In: Symposium on Principles of Programming Languages (POPL), pp. 4–16 (January 2002)
Arnold, M., Vechev, M., Yahav, E.: QVM: an efficient runtime for detecting defects in deployed systems. In: OOPSLA, pp. 143–162. ACM Press, New York (2008)
Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, J., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: abc: An extensible AspectJ compiler. In: AOSD, pp. 87–98 (March 2005)
Avgustinov, P., Tibble, J., Bodden, E., Lhoták, O., Hendren, L., de Moor, O., Ongkingco, N., Sittampalam, G.: Efficient trace monitoring. Tech. Rep. abc-2006-1 (March 2006), http://www.aspectbench.org/
Avgustinov, P., Tibble, J., de Moor, O.: Making trace monitors feasible. In: OOPSLA, pp. 589–608 (October 2007)
Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: OOPSLA, pp. 301–320 (October 2007)
Bodden, E.: J-LO - A tool for runtime-checking temporal assertions. Master’s thesis, RWTH Aachen University (November 2005), http://www.bodden.de/pubs/
Bodden, E.: Verifying finite-state properties of large-scale programs. Ph.D. thesis, McGill University (June 2009), available through ProQuest, http://www.bodden.de/pubs/
Bodden, E.: Efficient hybrid typestate analysis by determining continuation-equivalent states. In: ICSE 2010: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, pp. 5–14. ACM, New York (2010)
Bodden, E., Chen, F., Roşu, G.: Dependent advice: A general approach to optimizing history-based aspects. In: AOSD, pp. 3–14 (March 2009)
Bodden, E., Hendren, L.J., Lam, P., Lhoták, O., Naeem, N.A.: Collaborative runtime verification with tracematches. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 22–37. Springer, Heidelberg (2007)
Bodden, E., Hendren, L.J., Lam, P., Lhoták, O., Naeem, N.A.: Collaborative runtime verification with tracematches. Journal of Logics and Computation (November 2008), doi:10.1093/logcom/exn077
Bodden, E., Hendren, L.J., Lhoták, O.: A staged static program analysis to improve the performance of runtime monitoring. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 525–549. Springer, Heidelberg (2007)
Bodden, E., Lam, P., Hendren, L.: Finding Programming Errors Earlier by Evaluating Runtime Monitors Ahead-of-Time. In: Symposium on the Foundations of Software Engineering (FSE), pp. 36–47 (November 2008)
Bodden, E., Lam, P., Hendren, L.: Object representatives: a uniform abstraction for pointer information. In: Visions of Computer Science - BCS International Academic Conference. British Computing Society (September 2008), http://www.bcs.org/server.php?show=ConWebDoc.22982
Bodden, E., Lam, P., Hendren, L.: Clara: a Framework for Statically Evaluating Finite-state Runtime Monitors. In: Rosu, G., Sokolsky, O. (eds.) RV 2010. LNCS, vol. 6418, pp. 74–88. Springer, Heidelberg (2010)
Chen, F., Roşu, G.: MOP: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588 (October 2007)
Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of maude. Electronic Notes in Theoretical Computer Science (ENTCS) 4 (1996)
Dahm, M.: BCEL, http://jakarta.apache.org/bcel
DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)
Dwyer, M.B., Clarke, L.A., Cobleigh, J.M., Naumovich, G.: Flow analysis for verifying properties of concurrent software systems. ACM Transactions of Software Engineering and Methodolology (TOSEM) 13(4), 359–430 (2004)
Dwyer, M.B., Diep, M., Elbaum, S.: Reducing the cost of path property monitoring through sampling. In: ASE, Washington, DC, USA, pp. 228–237 (2008)
Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis: Exploiting static analysis results to reformulate and reduce the cost of dynamic analysis. In: ASE, pp. 124–133 (May 2007)
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering (TSE) 27(2), 99–123 (2001)
Fink, S., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. In: International Symposium on Software Testing and Analysis (ISSTA), pp. 133–144 (July 2006)
Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)
Gabel, M., Su, Z.: Javert: fully automatic mining of general temporal properties from dynamic traces. In: Symposium on the Foundations of Software Engineering (FSE), pp. 339–349 (November 2008)
Gabel, M., Su, Z.: Online inference and enforcement of temporal properties. In: ICSE 2010: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, pp. 15–24. ACM, New York (2010)
Goldsmith, S., O’Callahan, R., Aiken, A.: Relational queries over program traces. In: OOPSLA, pp. 385–402 (October 2005)
Hangal, S., Lam, M.S.: Tracking down software bugs using automatic anomaly detection. In: ICSE, pp. 291–301 (May 2002)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
Li, Z., Zhou, Y.: PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code. In: Symposium on the Foundations of Software Engineering (FSE), pp. 306–315 (September 2005)
Lo, D., Maoz, S.: Specification mining of symbolic scenario-based models. In: Workshop on Program analysis for software tools and engineering (PASTE), pp. 29–35 (November 2008)
Martin, M., Livshits, B., Lam, M.S.: Finding application errors using PQL: a program query language. In: OOPSLA, pp. 365–383 (October 2005)
Naeem, N.A., Lhoták, O.: Typestate-like analysis of multiple interacting objects. In: OOPSLA, pp. 347–366 (October 2008)
Pradel, M., Gross, T.R.: Automatic generation of object usage specifications from large method traces. In: ASE, pp. 371–382. IEEE Computer Society, Washington (2009)
Stolz, V., Huch, F.: Runtime verification of concurrent haskell programs. Electronic Notes in Theoretical Computer Science (ENTCS) 113, 201–216 (2005)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering (TSE) 12(1), 157–171 (1986)
Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: CASCON, p. 13. IBM Press (1999)
Walker, R., Viggers, K.: Implementing protocols via declarative event patterns. In: Symposium on the Foundations of Software Engineering (FSE), pp. 159–169 (October 2004)
Wasylkowski, A., Zeller, A., Lindig, C.: Detecting object usage anomalies. In: Symposium on the Foundations of Software Engineering (FSE), pp. 35–44 (September 2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodden, E., Lam, P. (2010). Clara: Partially Evaluating Runtime Monitors at Compile Time. In: Barringer, H., et al. Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol 6418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16612-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-16612-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16611-2
Online ISBN: 978-3-642-16612-9
eBook Packages: Computer ScienceComputer Science (R0)