MOrc Help

Please note that this is a preliminary, work-in-progress documentation of MOrc.

About MOrc

MOrc is a web-based tool for the formal analysis and verification of Orc programs. Formal analysis is performed using the rewriting logic specification of Orc and Real-Time Maude, a real-time extension of Maude, which is a high-performance engine for rewriting logic specifications. MOrc attempts to provide an easily accessible tool for formally analyzing Orc programs by hiding lower-level details pertaining to term rewriting and and the Maude tool.

The MOrc tool has been developed as part of a research project on rewriting-based formal semantics of Orc and the formal verification of Orc programs by Musab AlTurki and José Meseguer at the University of Illinois at Urbana-Champaign, with collaboration with Jayadev Misra and colleagues at the University of Texas at Austin.

Currently, MOrc is still under development. Some additional functionality, including most notably enhancements to post-processing of Real-Time Maude output, is yet to be implemented. The following sections describe briefly the main features of MOrc and how they can be used.

Admissible Orc Syntax

The top-left pane of MOrc's interface presents a text area in which the subject Orc program or expression can be specified. The user may also use one of the provided examples on the list of examples on the right. Clicking one of these examples loads the corresponding Orc specification in the input area, which may then be edited or used as is. An Orc program or expression can be specified according to the following BNF grammar.

<program> ::= <declarations> ; <expression> | <expression> <declarations> ::= <declarations> ; <declaration> | <declaration> <declaration> ::= ID ( ) := <expression> | ID ( <call_expr_list> ) := <expression> <expression> ::= <expression> | <expression> | <expression> > ID > <expression> | <expression> >> <expression> | <expression> < ID < <expression> | <expression> << <expression> | <expression> ; <expression> // to be added | ( <expression> ) | <call_expr_list> | zero <call_expr_list> ::= <call_expr_list> , <call_expr> | <call_expr> <call_expr> ::= ID ( <call_expr_list> ) | <local_call_expr> | ID | NUMBER | STRING | 'signal' | 'true' | 'false' <local_call_expr> ::= ID [ NUMBER ] | <call_expr> <infix_bin_sn> <call_expr> | <infix_un_sn> <call_expr> | <prefix_bin_sn> ( <call_expr> , <call_expr> ) <infix_bin_sn> ::= '+' | '-' | '*' | '/' | '%' | '==' | '>' | '>=' | '<' | '<=' | '!=' | '&&' | '||' <infix_un_sn> ::= '!' <prefix_bin_sn> ::= 'min' | 'max'

The tokens "ID", "NUMBER", and "STRING" have the following regular expression definitions.

ID [a-zA-Z][a-zA-Z0-9]* NUMBER [0-9][0-9]* STRING \"([^\"\\\n\t])*\"

Custom Sites

TBA

Simulation

The simulation analysis panel implements Real-Time Maude's timed rewrite command "trew" (see the Real-Time Maude manual). For simulating Orc programs, one or more limits on the simulation task may optionally be specified, which are particularly useful for simulating non-terminating Orc programs. The possible simulation limits are:

  1. Logical time limit: an upper bound on the logical time value of the state of the program.
  2. Publications limit: an upper bound on the number of publications allowed before stopping the simulation
  3. Rewrite steps limit: an upper bound on the number of rewrite steps allowed, where a rewrite step corresponds to a transition in the semantics of Orc (i.e. an application of one of the rewrite rules in the rewriting semantics of Orc: a site call, an expression call, a publishing of a value, a site return, or a time tick transition).

If more than one constraint is specified, the combined constraint is determined as their disjunction. Finally, the timeout field, which is a required field, is used to specify a timeout - in seconds - on the Real-Time Maude rewriting process.

Breadth-first Search

The search analysis panel implements timed and non-timed breadth-first search commands "tsearch" and "utsearch" of Real-Time Maude. The options for search are categorized as follows.

Search Type

The search is either timed, using "tsearch", or non-timed, using "utsearch". Timed search takes into account explicit time-stamps of states, and allows reasoning about timed properties of the timed transition system of the subject Orc program, such the number of publications within the first t time units, the time a specific value is published, or whether a pattern is reachable after a given timeout. When timed search is selected, the user may specify the type and value of the search time bound, or leave it unspecified for a timed search with no time limit.

Non-timed search, on the other hand, ignores time-stamps on states and, thus, allows for a more efficient analysis (due to the potentially smaller reachable state space), but at the expense of a slightly less expressive reasoning ability.

Search Parameters

The configurable search parameters include:

  1. Maximum number of solutions: an optional upper bound on the number of solutions to find. If left blank, the tool will try to find all possible solutions.
  2. Search timeout: the timeout - in seconds - on the Real-Time Maude process performing the search.
  3. Terminal states: if checked, the search will only consider solutions corresponding to terminal (deadlocked) states (i.e. states that cannot be further rewritten). By default, if not checked, the search considers all states reachable by one or more rewrite steps.

Orc Expression Pattern

The user may optionally specify an Orc expression pattern that a solution state must satisfy. When specified, the search command will look for states whose Orc expression components match at the top the given pattern.

An Orc expression pattern can be a concrete Orc program specified according to the Orc syntax BNF grammar above, for example "let(x)" and "if(x == y) >> let(true)", or a symbolic pattern containing pattern meta-variables ranging over terms of appropriate types. Syntactically, a pattern meta-variable is an identifier of the form $[A-Z][A-Z]?[0-9]*, where the prefix dollar sign $ distinguishes pattern variables from Orc variables, and the first one or two uppercase letters specify the type of the terms over which the pattern meta-variable ranges. Currently, the following pattern variables can be used:

$F[0-9]* ranges over Orc expressions $E[0-9]* ranges over expression names $M[0-9]* ranges over site names $V[0-9]* ranges over values $VL[0-9]* ranges over lists of values $X[0-9]* ranges over variables $XL[0-9]* ranges over lists of variables $P[0-9]* ranges over parameters $PL[0-9]* ranges over lists of parameters

For example, the following represent valid, non-concrete Orc expression patterns:

$F1 > $X > $F2 matches a sequential composition expression $F | $F matches a parallel composition of two identical subexpressions $M($VL) | $F matches an enabled site call composed in parallel with another expression $E(1, $P) matches an expression call with two parameters, the first of which is 1

Orc expression patterns can used with either timed or non-timed search.

Publication Constraints

The last section of the search analysis panel offers the ability to specify further solution state constraints relating to publication of values. In particular, an upper bound on the number of publications may be specified so that the search command may only consider reachable states satisfying the given bound.

Furthermore, timed constraints (for timed search) or non-timed constraints (for non-timed search) can also be specified on what values are published (Type I constraints) or the number of values published (Type || constraints) in a state. A constraint of either type, which is internally translated into a state predicate, can be added by pressing the corresponding "plus" button, and filling in the constraint parameters (Any constraint with missing or invalid input values is ignored). For a search task, the solution states will have to satisfy all the specified publication constraints (i.e., the conjunction of the corresponding state predicates).

Model Checking Linear Temporal Logic Formulas

The model checking analysis panel implements non-timed and time-bounded linear temporal logic (LTL) model checking command "mc" of Real-Time Maude. The options for model checking are categorized as follows.

Model Checking Parameters

As for search, model checking is either non-timed, in which state time-stamps are abstracted away, or time-bounded (normally) with a given time bound, in which a property is checked in the reachable (timed) state space up to the given time bound. For efficiency of analysis, non-timed model checking is based on a version of the semantics of Orc in which publication traces are not kept in the state, which implies that properties that can be verified for this type of model checking cannot refer to what or how many publications are made. This is in contrast to time-bounded model checking, for which properties may refer to both publications and the structure of the expression. Other parameters include specifying: (1) an optional upper bound on the number of publications, which restricts the analysis to the subset of the reachable state space satisfying this bound, and (2) a model checking timeout, which is required, on the Real-Time Maude process.

Property to Check

The LTL property can be either the generic deadlock-freeness property (a safety property that stipulates that no reachable state is terminal, or deadlocked), or, alternatively, a custom, user-defined formula, possibly based on user-defined atomic predicates. When the custom LTL property radio button is pressed, the form fields for specifying the property and any atomic predicates are shown, which are described next.

Atomic Predicates

This section allows the user to add and define custom, named atomic predicates on states, which may then be used in the specification of the LTL formula to be model-checked. Three types of atomic predicates can be specified:

  1. Expression pattern predicate: specifies a predicate that is true in a state whose expression component matches the given pattern at the top. The pattern can be specified as described above (here).
  2. Publication predicate: specifies a predicate that is true in a state in which the given value is published within the given time constraints. This predicate is only meaningful for time-bounded model checking.
  3. Publication length predicate: specifies a predicate that is true in a state in which at least the given number of publications are made within the given time constraints. This predicate is also only meaningful for time-bounded model checking.
For an atomic predicate to used in the LTL formula, it has to be given a name, which can be entered in the textfield following the "models" sign ⊨.

LTL Formula

The LTL formula field, which is a required field when specifying a custom formula, allows for specifying an LTL formula that may make use of user-defined atomic predicates according to the following syntax:

<formula> ::= 'True' | 'False' | AP (* An atomic proposition *) | 'O' <formula> (* Next *) | <formula> 'U' <formula> (* Until *) | '<>' <formula> (* Eventually *) | '[]' <formula> (* Always *) | <formula> 'W' <formula> (* Weak until *) | <formula> 'R' <formula> (* Release *) | <formula> '/\' <formula> (* And *) | <formula> '\/' <formula> (* Or *) | '~' <formula> (* Not | <formula> '->' <formula> (* Implies *) | <formula> '<->' <formula> (* Equivalent *) | <formula> '|->' <formula> (* Leads to *) | <formula> '=>' <formula> (* Always implies *) | <formula> '<=>' <formula> (* Always equivalent *)

In addition to the user-defined predicates above, the set of atomic predicates AP currently includes as a predefined predicate (that may also be used in the specification of the LTL formula) the predicate "deadlock", which is true in deadlocked states.

Feedback

For any technical questions or suggestions about MOrc, or this web site, please contact Musab AlTurki at alturki [at] illinois.edu. Thank you.