Mop

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Mop: an efficient and generic runtime verification framework

Full text

Pdf (351 KB)

Source

Conference on Object Oriented Programming Systems Languages and Applications archive
Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications table of contents

Montreal, Quebec, Canada

SESSION: Runtime techniques table of contents

Pages: 569 - 588

Year of Publication: 2007

ISBN:978-1-59593-786-5

Also published in ...

Authors

Feng Chen	University of Illinois at Urbana-Champaign, Urbana, IL
Grigore Roşu	University of Illinois at Urbana-Champaign, Urbana, IL

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 15

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1297027.1297069 What is a DOI?

ABSTRACT

Monitoring-Oriented Programming (MOP1) [21, 18, 22, 19] is a formal framework for software development and analysis, in which the developer specifies desired properties using definable specification formalisms, along with code to execute when properties are violated or validated. The MOP framework automatically generates monitors from the specified properties and then integrates them together with the user-defined code into the original system.

The previous design of MOP only allowed specifications without parameters, so it could not be used to state and monitor safety properties referring to two or more related objects. In this paper we propose a parametric specification formalism-independent extension of MOP, together with an implementation of JavaMOP that supports parameters. In our current implementation, parametric specifications are translated into AspectJ code and then weaved into the application using off-the-shelf AspectJ compilers; hence, MOP specifications can be seen as formal or logical aspects.

Our JavaMOP implementation was extensively evaluated on two benchmarks, Dacapo [14] and Tracematches [8], showing that runtime verification in general and MOP in particular are feasible. In some of the examples, millions of monitor instances are generated, each observing a set of related objects. To keep the runtime overhead of monitoring and event observation low, we devised and implemented a decentralized indexing optimization. Less than 8% of the experiments showed more than 10% runtime overhead; in most cases our tool generates monitoring code as efficient as the hand-optimized code. Despite its genericity, JavaMOP is empirically shown to be more efficient than runtime verification systems specialized and optimized for particular specification formalisms. Many property violations were detected during our experiments; some of them are benign, others indicate defects in programs. Many of these are subtle and hard to find by ordinary testing.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	P. Abercrombie and M. Karaorman. jContractor: Bytecode instrumentation techniques for implementing DBC in Java. In RV'02, volume 70.4 of ENTCS, 2002
	2	Chris Allan , Pavel Avgustinov , Aske Simon Christensen , Laurie Hendren , Sascha Kuzins , Ondřej Lhoták , Oege de Moor , Damien Sereni , Ganesh Sittampalam , Julian Tibble, Adding trace matching with free variables to AspectJ, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	3	C. Anley. Advanced SQL injection in SQL server applications. NGSSoftware, 2002.
	4	AspectC++. http://www.aspectc.org/.
	5	C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, and W. Visser. Experiments with test case generation and runtime analysis. In ASM'03, volume 2589 of LNCS, pages 87--107, 2003.
	6	P. Avgustinov, E. Bodden, E. Hajiyev, L. Hendren, O. Lhotak, O. de Moor, N. Ongkingco, D. Sereni, G. Sittampalam, J. Tibble, and M. Verbaere. Aspects for trace monitoring. In FATES/RV'06, volume 4262 of LNCS, pages 20--39, 2006.
	7	Pavel Avgustinov , Aske Simon Christensen , Laurie Hendren , Sascha Kuzins , Jennifer Lhoták , Ondřej Lhoták , Oege de Moor , Damien Sereni , Ganesh Sittampalam , Julian Tibble, abc: an extensible AspectJ compiler, Proceedings of the 4th international conference on Aspect-oriented software development, p.87-98, March 14-18, 2005, Chicago, Illinois [doi>10.1145/1052898.1052906]
	8	P. Avgustinov, J. Tibble, E. Bodden, O. Lhotak, L. Hendren, O. de Moor, N. Ongkingco, and G. Sittampalam. Efficient Trace Monitoring. Technical Report abc-2006-1, Oxford University, 2006.
	9	Pavel Avgustinov , Julian Tibble , Oege de Moor, Making trace monitors feasible, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
	10	M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS'04, volume 3362 of LNCS, pages 49--69, 2004.
	11	H. Barringer, B. Finkbeiner, Y. Gurevich, and H. Sipma. Runtime Verification (RV'05). Elsevier, 2005. ENTCS 144.
	12	H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-Based Runtime Verification. In VMCAI'04, volume 2937 of LNCS, pages 44--57, 2004.
	13	D. Bartetzko, C. Fischer, M. Moller, and H. Wehrheim. Jass-Java with Assertions. In RV'01, volume 55.2 of ENTCS, 2001.
	14	Stephen M. Blackburn , Robin Garner , Chris Hoffmann , Asjad M. Khang , Kathryn S. McKinley , Rotem Bentzur , Amer Diwan , Daniel Feinberg , Daniel Frampton , Samuel Z. Guyer , Martin Hirzel , Antony Hosking , Maria Jump , Han Lee , J. Eliot B. Moss , B. Moss , Aashish Phansalkar , Darko Stefanović , Thomas VanDrunen , Daniel von Dincklage , Ben Wiedermann, The DaCapo benchmarks: java benchmarking development and analysis, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
	15	E. Bodden. J-LO, a tool for runtime-checking temporal assertions. PhD thesis, RWTH Aachen University, 2005.
	16	E. Bodden, L. Hendren, and O. Lhot2ak. A staged static program analysis to improve the performance of runtime monitoring. In ECOOP'07, volume 4609 of LNCS, pages 525--549, 2007.
	17	E. Bodden, P. Lam, and L. Hendren. Flow-sensitive static optimizations for runtime monitors. Technical Report abc-2007-3, Oxford University, 2007.
	18	F. Chen, M. D'Amorim, and G. Roşu. A formal monitoringbased framework for software development and analysis. In ICFEM'04, volume 3308 of LNCS, pages 357--373, 2004.
	19	F. Chen, M. D'Amorim, and G. Roşu. Checking and correcting behaviors of Java programs at runtime with JavaMOP. In RV'05, volume 144(4) of ENTCS, 2005.
	20	F. Chen and G. Roşu. JavaMOP. http://fsl.cs.uiuc.edu/javamop.
	21	F. Chen and G. Roşu. Towards monitoring-oriented programming: A paradigm combining specification and implementation. In RV'03, volume 89(2) of ENTCS, 2003.
	22	F. Chen and G. Roşu. Java-MOP: A monitoring oriented programming environment for Java. In TACAS'05, volume 3440 of LNCS, pages 546--550, 2005.
	23	Marcelo d'Amorim , Klaus Havelund, Event-based runtime verification of java programs, Proceedings of the third international workshop on Dynamic analysis, p.1-7, May 17-17, 2005, St. Louis, Missouri
	24	D. Drusinsky. Temporal Rover. http://www.time-rover.com.
	25	Eclipse. http://eclipse.org.
	26	Eiffel Language. http://www.eiffel.com/.
	27	Simon F. Goldsmith , Robert O'Callahan , Alex Aiken, Relational queries over program traces, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	28	K. Havelund and G. Roşu. Monitoring Java programs with Java PathExplorer. In RV'01, volume 55.2 of ENTCS, 2001.
	29	K. Havelund and G. Roşu. Runtime Verification (RV'01, RV'02, RV'04). Elsevier, 2001, 2002, 2004. ENTCS 55, 70,113.
	30	C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
	31	JBoss. http://www.jboss.org.
	32	jHotdraw. http://www.jhotdraw.org.
	33	G. Kiczales, J. Lamping, A. Menhdhekar, C. Maeda, C. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-Oriented programming. In ECOOP'97, volume 1241 of LNCS, pages 220--242, 1997.
	34	Gregor Kiczales , Jim Des Rivieres, The Art of the Metaobject Protocol, MIT Press, Cambridge, MA, 1991
	35	M. Kim, S. Kannan, I. Lee, and O. Sokolsky. Java-MaC: a Runtime Assurance Tool for Java. In RV'01, volume 55.2 of ENTCS, 2001.
	36	Gary T. Leavens , Clyde Ruby , K. Rustan , M. Leino , Erik Poll , Bart Jacobs, JML (poster session): notations and tools supporting detailed design in Java, Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), p.105-106, January 2000, Minneapolis, Minnesota, United States [doi>10.1145/367845.367996]
	37	Lucene. http://lucene.apache.org.
	38	Michael Martin , Benjamin Livshits , Monica S. Lam, Finding application errors and security flaws using PQL: a program query language, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	39	Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
	40	Martin Rinard, Acceptability-oriented computing, Companion of the 18th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 26-30, 2003, Anaheim, CA, USA [doi>10.1145/949344.949402]
	41	O. Sokolsky and M. Viswanathan. Runtime Verification (RV'03). Elsevier, 2003. ENTCS 89.
	42	Xalan. http://xml.apache.org/xalan-j/.

CITED BY 16

	Andreas Sewe , Christoph Bockisch , Mira Mezini, Redundancy-free residual dispatch: using ordered binary decision diagrams for efficient dispatch, Proceedings of the 7th workshop on Foundations of aspect-oriented languages, p.1-7, April 01-01, 2008, Brussels, Belgium
	Pavel Avgustinov , Julian Tibble , Oege de Moor, Making trace monitors feasible, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Lu Yang , Jianwen Tang , Jianhua Zhao , Xuandong Li, A case study for monitoring-oriented programming in multi-core architecture, Proceedings of the 1st international workshop on Multicore software engineering, May 11-11, 2008, Leipzig, Germany
	Isil Dillig , Thomas Dillig , Eran Yahav , Satish Chandra, The CLOSER: automating resource management in java, Proceedings of the 7th international symposium on Memory management, June 07-08, 2008, Tucson, AZ, USA
	Matthew Arnold , Martin Vechev , Eran Yahav, QVM: an efficient runtime for detecting defects in deployed systems, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Domenico Bianculli , Carlo Ghezzi, Towards a methodology for lifelong validation of service compositions, Proceedings of the 2nd international workshop on Systems development in SOA environments, May 11-11, 2008, Leipzig, Germany
	Feng Chen , Traian Florin Serbanuta , Grigore Rosu, jPredictor: a predictive runtime analysis tool for java, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Nomair A. Naeem , Ondrej Lhotak, Typestate-like analysis of multiple interacting objects, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Madhu Gopinathan , Sriram K. Rajamani, Enforcing object protocols by combining static and runtime analysis, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Michael Gorbovitski , Tom Rothamel , Yanhong A. Liu , Scott D. Stoller, Efficient runtime invariant checking: a framework and case study, Proceedings of the 2008 international workshop on dynamic analysis: held in conjunction with the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2008), July 21-21, 2008, Seattle, Washington
	Eric Bodden , Feng Chen , Grigore Rosu, Dependent advice: a general approach to optimizing history-based aspects, Proceedings of the 8th ACM international conference on Aspect-oriented software development, March 02-06, 2009, Charlottesville, Virginia, USA
	Amjad Nusayr, AOP as a formal framework for runtime monitoring, Proceedings of the 2008 Foundations of Software Engineering Doctoral Symposium, p.25-28, November 10-10, 2008, Atlanta, Georgia
	Amjad Nusayr , Jonathan Cook, AOP for the domain of runtime monitoring: breaking out of the code-based model, Proceedings of the 4th workshop on Domain-specific aspect languages, March 03-03, 2009, Charlottesville, Virginia, USA
	Maria Jump , Kathryn S. McKinley, Dynamic shape analysis via degree metrics, Proceedings of the 2009 international symposium on Memory management, June 19-20, 2009, Dublin, Ireland
	Rohit Chadha , A. Prasad Sistla , Mahesh Viswanathan, On the expressiveness and complexity of randomization in finite state monitors, Journal of the ACM (JACM), v.56 n.5, p.1-44, August 2009
	Eric Bodden , Reehan Shaikh , Laurie Hendren, Relational aspects as tracematches, Proceedings of the 7th international conference on Aspect-oriented software development, March 31-April 04, 2008, Brussels, Belgium