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); and as a lightweight formal method.

[edit] 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
		FSM	ERE	CFG	PTLTL	FTLTL	PTCaRet	...
	JavaMOP	JavaFSM	JavaERE	JavaCFG	JavaPTLTL	JavaFTLTL	JavaPTCaRet	...
	BusMOP	BusFSM	BusERE	...	BusPTLTL	...	...	...
	...	...	...	...	...	...	...	...
	MOP Matrix: a clickable map of MOP pages.

[edit] 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;

[edit] 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 used in various other monitoring applications. Below is a list containing our current logic plugins. Each plugin can be experimented with online before download.

• FSM -- Finite State Machines
• 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

[edit] MOP Tutorial Slides

These slides provide an overview of the MOP project. Tutorial Slides

Another presentation, given at Microsoft Research in 2007. MSR Presentation

[edit] Select MOP Publications

Below is a list of the papers most relevant to MOP, in reverse chronological order. A complete list of all papers related to MOP can be found HERE.

• The paper that introduced the fully general, parametric monitoring algorithm for JavaMOP:

Parametric Trace Slicing and Monitoring 

Feng Chen and Grigore Rosu
TACAS'09, LNCS 5505, pp 246-261. 2009.
PDF, Slides (PPT), LNCS, TACAS'09, DBLP, BIB

• The paper that introduced BusMOP, extending MOP to PCI Bus traffic monitoring:

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

Rodolfo Pellizzoni, Patrick Meredith, Marco Caccamo and Grigore Rosu
RTSS'08, IEEE, pp. 481-491. 2008
PDF, Experiments, RTSS'08 slides, RTSS'08, BIB

• The paper that introduced the original parametric monitoring algorithm for JavaMOP:

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

• The paper that originally introduced MOP:

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