MOP4 Syntax

Links:
MOP

The syntax below uses BNF. Since MOP is generic and can be instantiated, the MOP syntax is composed of three kinds of constructs: generic, language-specific, and logic-specific. We define the generic constructs on this page and also describe which constructs need to be instantiated for a specific MOP instance.

// BNF below is extended with {p} for zero or more and [p] for zero or one

// The generic syntax
   <Specification>             ::= {<Language Modifier>} <Id> <Language Parameters> "{"
                                       {<Language Declaration>}
                                       {<Event>}
                                       {  <Property>
                                         {<Property Handler>}
                                       }
                                   "}"
   <Event>                     ::= ["creation"] "event" <Id> <Language Event Definition>
                                   <Language Action> 
   <Property>                  ::= <Logic Name> ":" <Logic Syntax>
   <Property Handler>          ::= "@" <Logic State> <Language Action> 

// The language-specific syntax
   <Language Modifier>         ::= <Id>
   <Language Parameters>       ::= // syntax of parameter list in underlying language        
   <Language Declaration>      ::= // syntax of declaration in the underlying language       
   <Language Event Definition> ::= // syntax used to specify when to trigger an event        
   <Language Action>           ::= // syntax describing an action in the underlying language 
   <Language Statements>       ::= // syntax of statements in the underlying language        

// The logic-plugin-specific syntax
   <Logic Name>                ::= <Id>
   <Logic Syntax>              ::= // the requirements syntax provided by the logic plugin above
   <Logic State>               ::= // identifiers denoting states to which handlers can be
                                      associated, e.g., violation

Generic Syntactic Constructs

The following syntactic constructs are shared by different MOP instances:

<Specification>

<Specification> describes the generic MOP specification syntax, which can be instantiated for MOP language instances and MOP logic plugins.

<Event>

The event declaration code allows for the definition of events which may then be referred to in the property (<Property>). Event declarations can also have arbitrary code associated with them (<Language Action>), which is run when the event is observed (<Language Event Definition>), e.g. code to modify the program or the monitor state.

<Property>

Every MOP specification may contain zero or more properties. A property consists of a named formalism (<Logic Name>), followed by a colon, followed by a property specification using the named formalism (<Logic Syntax>) and usually referring to the declared events.

If the property is missing, then the MOP specification is called raw. Raw specifications are useful when no existing logic plugin is powerful or efficient enough to specify the desired property; in that case, one embeds the custom monitoring code manually within the event generation code.

<Property Handler>

Handlers contain arbitrary code from the source language, and are invoked when a certain logic state (<Logic State>) is reached, e.g., validation, violation, or a particular state in a finite state machine description.

Language-Specific Syntactic Constructs

These are syntactic constructs that need to be instantiated by every MOP language instance according. The following links show how they are instantiated for current MOP language instances:

JavaMOP Syntax -- MOP for Java Programs
BusMOP Syntax -- MOP for the PCI Bus, using Verilog and VHDL

<Language Modifier>

<Language Modifier>s are specific to each language instance of MOP. Syntactically, they can be any valid identifier restricted by the given language. They change the behavior of the generated monitoring code.

<Language Parameters>

<Language Parameters> allow one to define the parameters of a parametric specification using the language corresponding to the MOP instance. Not all MOP instances are parametric, however, so not all instances must define this category.

<Language Declaration>

<Language Declaration>s are specific to each language instance of MOP. They allow for the declaration of monitor local variables.

<Language Event Definition>

<Language Event Definition>s are specific to each language instance of MOP. They define the conditions under which an event is triggered.

<Language Action>

Events and handlers can have arbitrary code associated with them, called an action. The action is run when the event is observed, or the handler triggered. An action can modify the program or the monitor state.

<Language Statements>

<Language Statements> are specific to each language instance of MOP. They are used for event actions, arbitrary code that is executed when an event triggers, and property handlers.

Logic-Specific Syntactic Constructs

These are syntactic constructs that need to be instantiated by every logic plugin. The following links show how they are instantiated for current MOP logic plugins:

FSM Syntax -- Finite State Machine Descriptions
ERE Syntax -- Extended Regular Expressions
CFG Syntax -- Context Free Grammars
PTLTL Syntax -- Past Time Linear Temporal Logic
LTL Syntax -- Linear Temporal Logic
PTCaRet Syntax -- Past Time Linear Temporal Logic with Calls and Returns
SRS Syntax -- String Rewriting Systems

<Logic Name>

An identifier to indicate in which logic a property is defined.

<Logic Syntax>

This refers to the syntax of the actual property definition, and is defined on the syntax page for each plugin.

<Logic State>

<Logic State>s are constants defined for each plugin, telling for which monitor states a handler may be written.