Publications on Monitoring-Oriented Programming

From FSL
Jump to: navigation, search

There is a series of papers on Monitoring-Oriented Programming (MOP). They are all listed on this page in reverse chronological order. See the MOP project page for a brief introduction to MOP, as well as for the latest progress and implementations.

Contents

OOPSLA'07

MOP: An Efficient and Generic Runtime Verification Framework
Feng Chen and Grigore Rosu
OOPSLA'07, ACM press, pp 569-588. 2007
Abstract. Monitoring-Oriented Programming (MOP) 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 and Tracematches, 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.
PDF, OOPSLA'07 slides, ACM, OOPSLA'07, DBLP, TR@UIUC, BIB

2006 Technical report

MOP: Reliable Software Development using Abstract Aspects
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2006-2776, October 2006
Abstract. Monitoring-Oriented Programming (MOP) is a formal framework for software development and analysis. It aims at reducing the gap between formal specification and implementation via runtime monitoring. In MOP, the developer specifies desired properties using definable specification formalisms, along with code to execute when properties are violated or validated, which can be used not only to report, but especially to recover from errors. The MOP framework automatically generates monitors from the specified properties and then integrates them together with the recovery code into the original system. Since the recovery code typically is executed infrequently and can be validated more easily than the actual system, MOP is expected to increase software reliability at little amortized runtime overhead. This paper presents MOP from a pragmatic, rather than foundational perspective, as an instance of aspect-oriented programming (AOP) where one defines abstract aspects using logics; one is relieved from providing unnecessary implementation details, because these are generated and integrated automatically. Existing AOP tools provide crucial support: an MOP frontend for Java, called JavaMOP and also discussed in the paper, is implemented using AspectJ. A series of examples illustrate the strengths of MOP from different perspectives.
PDF, TR@UIUC, BIB

RV'05

Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP
Feng Chen, Marcelo d'Amorim and Grigore Rosu
RV'05, ENTCS 144, issue 4, pp 3-20. 2005.
Abstract. Monitoring-oriented programming (MOP) is a software development and analysis technique in which monitoring plays a fundamental role. MOP users can add their favorite or domain-specific requirements specification formalisms into the framework by means of logic plug-ins, which essentially comprise monitor synthesis algorithms for properties expressed as formulae. The properties are specified together with declarations stating where and how to automatically integrate the corresponding monitor into the system, as well as what to do if the property is violated or validated. In this paper we present Java-MOP, an MOP environment for developping robust Java applications. Based upon a carefully designed property specification schema and upon several logic plug-ins, Java-MOP allows users to specify and monitor safety properties, which can refer not only to the current program state, but also to the entire execution trace of a program, including past and future behaviors.
PDF, ENTCS, RV'05, DBLP, BIB

TACAS'05

Java-MOP: A Monitoring Oriented Programming Environment for Java
Feng Chen and Grigore Rosu
TACAS'05, LNCS 3440, pp 546-550. 2005.
Abstract. A Java-based tool-supported software development and analysis framework is presented, where monitoring is a foundational principle. Expressive requirements specification formalisms can be included into the framework via logic plug-ins, allowing one to refer not only to the current state, but also to both past and future states.
PDF, LNCS, TACAS'05, DBLP, BIB

2004 Technical report

Monitoring-Oriented Programming: A Tool-Supported Methodology for Higher Quality Object-Oriented Software
Feng Chen, Marcelo d'Amorim and Grigore Rosu
Technical Report UIUCDCS-R-2004-2420, 2004.
Abstract. This paper presents a tool-supported methodological paradigm for object-oriented software development, called monitoring-oriented programming and abbreviated MOP, in which runtime monitoring is a basic software design principle. The general idea underlying MOP is that software developers insert specications in their code via annotations. Actual monitoring code is automatically synthesized from these annotations before compilation and integrated at appropriate places in the program, according to user-defined configuration attributes. This way, the specification is checked at runtime against the implementation. Moreover, violations and/or validations of specifications can trigger user-defned code at any points in the program, in particular recovery code, outputting or sending messages, or raising exceptions. The MOP paradigm does not promote or enforce any specific formalism to specify requirements: it allows the users to plug-in their favorite or domain-specic specification formalisms via logic plug-in modules. There are two major technical challenges that MOP supporting tools unavoidably face: monitor synthesis and monitor integration. The former is heavily dependent on the specification formalism and comes as part of the corresponding logic plug-in, while the latter is uniform for all specification formalisms and depends only on the target programming language. An experimental prototype tool, called Java-MOP, is also discussed, which currently supports most but not all of the desired MOP features. MOP aims at reducing the gap between formal specification and implementation, by integrating the two and allowing them together to form a system.
PDF, TR@UIUC, BIB

ICFEM'04

A Formal Monitoring-based Framework for Software Development and Analysis
Feng Chen and Marcelo d'Amorim and Grigore Rosu
ICFEM'04, LNCS 3308, pp 357 - 373. 2004.
Abstract. A formal framework for software development and analysis is presented, which aims at reducing the gap between formal specification and implementation by integrating the two and allowing them together to form a system. It is called monitoring-oriented programming (MOP), since runtime monitoring is supported and encouraged as a fundamental principle. Monitors are automatically synthesized from formal specifications and integrated at appropriate places in the program, according to user-configurable attributes. Violations and/or validations of specifications can trigger user-defined code at any points in the program, in particular recovery code, outputting/sending messages, or raising exceptions. The major novelty of MOP is its generality w.r.t. logical formalisms: it allows users to insert their favorite or domain-specific specification formalisms via logic plug-in modules. A WWW repository has been created, allowing MOP users to download and upload logic plug-ins. An experimental prototype tool, called Java-MOP, is also discussed, which currently supports most but not all of the desired MOP features.
PDF, LNCS, ICFEM'04, DBLP, BIB

RV'03

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation
Feng Chen and Grigore Rosu
RV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 108-127. 2003
Abstract. With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.
PDF, MOP, DOI, RV'03, BIB

Personal tools
Namespaces

Variants
Actions
Navigation