Monitoring-Oriented Programming

From FSL

Monitoring-Oriented Programming, abbreviated MOP, is a software development and analysis framework aiming at reducing the gap between formal specification and implementation by allowing them together to form a system. In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable software: monitors are automatically synthesized from specified properties and integrated into the original system to check its dynamic behaviors during execution. When a specification is violated or validated at runtime, user-defined actions will be triggered, which can be any code from information logging to runtime recovery.

One can understand MOP from at least three perspectives:

• As a discipline allowing one to improve safety, reliability and dependability of a system by monitoring its requirements against its implementation at runtime;
• As an extension of programming languages with logics. One can add logical statements anywhere in the program, referring to past or future states;
• As a lightweight formal method. While firmly based on logical formalisms and mathematical techniques, MOP may allow one to avoid or significantly reduce the complexity of verifying an implementation against its specification by simply not letting it go wrong at runtime.

The MOP Architecture

MOP has a special "layered" architecture designed for maximum code reuse. Logic plugins are shared between all instances of MOP by implementing shells, which are handled by the different MOP instances (currently JavaMOP and BusMOP). The top-most layer also allows for several different interfaces to MOP. The MOP Matrix below allows one to view the plugin and shell portions of the architecture.

The MOP Matrix

MOP is generic both in the underlying programming language and in the requirements specification formalism in which properties are expressed. The clickable table below shows all current instances of MOP and can be used to navigate MOP's webpages on this site. The rows show instances by the language and the columns instances by the logic. A cell "..." means that the corresponding combination is not yet available.

MOP

MOP Language Instances

• JavaMOP is an MOP tool for Java;
• BusMOP is an MOP tool for monitoring consumer off the shelf components over the PCI bus;

MOP Logic Plugins

Logic plugins implement and encapsulate monitor synthesis algorithms for particular requirements specification formalisms. While they are a core feature of MOP, logic plugins can be and are also used in various other monitoring applications. Below is a list containing our current logic plugins. Each plugin can be experimented with online before download.

• ERE -- Extended Regular Expressions
• CFG -- Context Free Grammars
• PTLTL -- Past Time Linear Temporal Logic
• FTLTL -- Future Time Linear Temporal Logic
• PTCARET -- Past Time LTL with Calls and Returns

Send us your logic plugin!

MOP Publications

Here is a list of relevant publications on MOP, with abstracts and additional information. Below is the list of all our publications that are directly or indirectly related to MOP, in reverse chronological order.

Efficient Monitoring of Parametric Context-Free Patterns 

Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
ASE'08, IEEE/ACM 2008, ACM Sigsoft Distinguished Paper
PDF, ASE'08 slides-key, ASE'08 slides-pdf, ASE'08 slides-ppt, ASE'08 slides-mov, ASE'08, BIB

Parametric Trace Slicing and Monitoring 

Grigore Rosu and Feng Chen
Technical report UIUCDCS-R-2008-2977, July 2008
PDF, TR@UIUC, BIB

Hardware Runtime Monitoring for Dependable COTS-based Real-Time Embedded Systems 

Rodolfo Pellizzoni, Patrick Meredith, Marco Caccamo and Grigore Rosu
RTSS'08, IEEE, to appear
PDF, BIB

Monitoring IVHM Systems using a Monitor-Oriented Programming Framework 

Sudipto Ghoshal, Solaiappan Manimaran, Grigore Rosu, Traian Florin Serbanuta, and Gheorghe Stefanescu
LFM 2008
PDF, LFM'08, PPT, BIB

Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns -- 

Grigore Rosu,Feng Chen and Thomas Ball
Technical report UIUCDCS-R-2007-2908, October 2007
PDF, BIB

MOP: An Efficient and Generic Runtime Verification Framework 

Feng Chen and Grigore Rosu
OOPSLA'07, ACM press, pp 569-588. 2007
PDF, OOPSLA'07 slides, ACM, OOPSLA'07, DBLP, TR@UIUC, BIB

On Safety Properties and Their Monitoring 

Grigore Rosu
Technical report UIUCDCS-R-2007-2850, February 2007
PDF, ZIP, TR@UIUC, BIB

MOP: Reliable Software Development using Abstract Aspects 

Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2006-2776, October 2006
PDF, TR@UIUC, BIB

Allen Linear (Interval) Temporal Logic -Translation to LTL and Monitor Synthesis- 

Grigore Rosu and Saddek Bensalem
CAV'06, LNCS 4144, pp 263-277, 2006
PDF, CAV'06, CAV'06 Slides, BIB

Efficient Monitoring of Omega-Languages 

Marcelo d'Amorim and Grigore Rosu
CAV'05, LNCS 3576, pp 364 - 378. 2005.
PDF, LNCS, CAV'05, DBLP, BIB

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.
PDF, ENTCS, RV'05, DBLP, BIB

Java-MOP: A Monitoring Oriented Programming Environment for Java 

Feng Chen and Grigore Rosu
TACAS'05, LNCS 3440, pp 546-550. 2005.
PDF, LNCS, TACAS'05, DBLP, BIB

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.
PDF, TR@UIUC, BIB

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.
PDF, LNCS, ICFEM'04, DBLP, BIB

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation 

Feng Chen and Grigore Rosu
RV'03, ENTCS 89, issue 2, pp 108 - 127. 2003.
PDF, ENTCS, RV'03, DBLP, BIB