Verification View

The Verification View provides 3 different methods to test a machine:

• Modelchecking,
• LTL Verifications and
• Symbolic Checking

In each tab you can add multiple tests to check you currently selected machine and interrupt the checking process by pressing the "Cancel" button.

Modelchecking

By pressing the plus button you can add several model checking variants. The following view will be shown:

Select one of the search strategies (breadth first, depth first or a mix of both) and the checkboxes containing different possible errors like deadlocks to be checked for. By pushing the "Model Check" button your selected variant will be added to the list shown at the top of the Modelchecking Tab.

LTL Verifications

By pressing the "Add LTL Formula" or "Add LTL Pattern" buttons an editor for each respectively will be opened and you can add LTL formulas or patterns to the lists to be checked for.

Summary of LTL Syntax supported by ProB

• use {...} for B predicates,
• G,F,X,U,W,R,true,false,not,&,or and => are part of the supported LTL syntax,
• use e(op) to check if an operation op is enabled,
• use deadlock to check if a state is deadlocked,
• use deadlock(op1,...,opk) with k>0 to check if all operations in the brackets are disabled,
• use controller(op1,...,opk) with k>0 to check if exactly one of the operations in the brackets is enabled,
• use deterministic(op1,...,opk) with k>0 to check if maximum one of the operations in the brackets is enabled,
• use sink to check if no operation is enabled that leads to another state,
• use brackets to check what is the next operation, e.g. [reset] => X{db={}},
• Past-LTL is supported: Y,H,O,S,T are the duals to X,G,F,U,R.

Setting Fairness Constraints

• Give fairness constraints by means of implication: fair => f, where "fair" are the fairness constraints and "f" is LTL-formula intended to be checked.
• Use WF(-) and SF(-) to set action-based weak and strong fairness constraints, respectively,
• use WEF and SEF to search for bad paths that are weakly and strongly fair with respect to all transitions, respectively.

Summary of LTL Patterns

• Supported types: Non negative whole numbers, sequences, LTL formula
• Definition of variables: <type> <identifier>: <value>
• Assignment of variables: <identifier>: <value>

• Scopes for variables: Loop, pattern, global (a lookup for a variable checks the inner scopes first until the variable is found)

• Definition of a Pattern:

    def `<name>` ( `<parameters>` ):
        `<body>`

The parameters are separated by a comma. Each parameter is of the form <identifier> : <type> The body contains statements such as definition or assignment of variables as well as loops. Patterns can be overloaded.

• Pattern Invocation: <name>( <arguments> )

Remark: Pattern Invocations do not depend on the order of the definitions of the used patterns. So patterns can be invocated before they are defined. Patterns can only be defined in the global scope. It is not possible to define patterns within other patterns.

• Loops:

    count `<identifier>`: `<start>` `<up/down>` to `<end>`:
        `<body>`
    end

The body must at least define or assign a variable.

• Definition of a sequence: ( <formulae> )

A sequence contains many formulae that must be true in different states. It is not required that the states must come one after another. must at least contain two formulae.

• Definition of a sequence with condition:

( <formulae> without <condition> ) <identifier> without <condition>

The first use case extends the definition of a sequence by an additional condition. The second use case requires to be a name of a variable with the datatype seq. The sequence stored in the variable are used to define a new sequence where the condition is true.

• Invocation of a sequence: seq( <argument> )

is a variable of the type seq or a definition of a sequence. Invoking a sequence returns a LTL formula.

• Scopes:

before(<right endpoint>, <property>) after(<left endpoint>, <property>) between(<left endpoint>, <right endpoint>, <property>) after_until(<left endpoint>, <right endpoint>, <property>)

The endpoints and properties must be regular LTL formulae. The return value of a scope is a regular LTL formula where the given conditions are true.

• One-line comment : // comment
• Multiline comment: /* comment */

Symbolic Checking

By pressing the plus button you can add several symbolic checking variants. The following view will be shown:

The dropdown menu allows you to select the type of check. Some variants of the symbolic checking might need additional parameters (e.g. Invariant needs an operation).