Checking CSP Assertions: Difference between revisions

As of version 1.3.4, ProB provides support for refinement checking and various other assertions (deadlock, divergence, determinism, and LTL/CTL assertions) of CSP-M specifications. In this tutorial we give a short overview of the ProB’s implementations and features for checking CSP assertions. In the Tcl/Tk interface of ProB, CSP assertions can be assembled and checked in the CSP Assertions Viewer. A description of the CSP Assertions Viewer is also given.

Supported CSP Assertions in ProB

ProB provides support for checking almost all types of CSP-M assertions that can be checked within FDR2. Besides the assertion types that can be checked in FDR2, in ProB one also can check temporal properties on processes expressed by means of LTL and CTL formulae.^[1] The following types of assertions are supported in ProB:

Refinement
Refinement is one of the fundamental notions for construction and verification of systems specified in CSP. Given two CSP processes P and Q one can state in ProB the property that process Q is an ‘m’ refinement of P by the following assertion declaration:

assert P [m= Q

where m indicates one of the following types of comparison: ‘T’ for traces, ‘F’ for failures, ‘FD’ for failures-divergence, ‘R’ for refusals, and ‘RD’ for ‘refusals-divergence’. Note that the refinement types ‘V’ (revivals) and ‘VD’ (revivals-divergence) that are part of the refinement assertions supported by FDR2 are yet not supported by ProB.

Deadlock
Stating assertions about CSP processes to be deadlock-free is possible by the following assertion declaration:

assert P :[deadlock free [m]]

where P is a process expression and m indicates one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).

Determinism
Stating assertions about CSP processes to be deterministic is possible by the following assertion declaration:

assert P :[deterministic [m]]

where P is a process expression and m one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).

Livelock
Stating assertions about CSP processes to be livelock-free is possible by the following assertion declaration:

assert P :[livelock free]

where P is a process expression.

Temporal Properties
In ProB it is also possible to make assertions about temporal properties of CSP processes both in LTL and CTL. Basically, one wants to check whether some process P satisfies a formula f expressed in temporal logic (denoted by P |= f).

To check whether a process P satisfies an LTL formula `f` write the following declaration:

assert P |= LTL: “f”

Note that f must be enclosed in quotes and that the satisfaction relation |= is immediately followed by `LTL:`. ProB supports LTL^[e], an extended version of LTL which provides additionally support for making propositions on transitions. The following LTL^[e] syntax for CSP-M specifications can be outlined by the following rules:

• Atomic propositions:
  • To check if an event `evt` is enabled in a state use `e(evt)`
• Transition propositions:
  • To check whether an event `evt` is executed use `[evt]`
• Logical operators
  • true and false
  • `not`: negation
  • `&`,`or`,and `=>`: conjunction, disjunction and implication
• Temporal operators:
  • `G f`: globally
  • `F f`: finally
  • `X f`: next
  • `f U g`: until
  • `f W g`: weak-until
  • `f R g`: release
• Fairness operators:
  • `WF(evt)` or `wf(evt)`: weak fairness, where `evt` is an event
  • `SF(evt)` or `sf(evt)`: strong fairness, where `evt` is an event
  • `WEF` and `SEF` for checking LTL[e] formulae on executions that are strongly and weakly fair with respect to all events, respectively

An LTL^[e] formula f is satisfied by some CSP process P if all executions of P satisfy f. If there is an execution of P which violates the property f, then the test P |= f fails by providing a counterexample. Depending on whether f expresses a safety or liveness property a finite path or a path in lasso-form (, i.e. a path leading to a cycle) is returned as a counterexample, respectively.

Note that ProB supports also Past-LTL^[e]. Past-LTL^[e], however, can be considered inappropriate be used in LTL assertions since the goal of this type of assertions is usually to check whether all executions starting at the initial states of the process satisfy the respective LTL[e].

To check whether a process P satisfies a CTL formula f the following assertion should be made:

assert P |= CTL: “f”

As for LTL, CTL formulae should be put in between quotes. The CTL syntax for CSP-M specifications could be summarized as follows:

• Atomic propositions:
  • To check if an event `evt` is enabled in a state use `e(evt)`
• Transition propositions:
  • To check whether an event `evt` is executed use `[evt]`
• State formulae, where f, f1 and f2 are path formulae:
  • true | false | `not` f | f1 `&` f2 | f1 `or` f2 | f1 `=>` f2,
  • E f : path quantifier \exists, pronounced `for some path`
  • A f : path quantifier \forall, pronounced `for all paths`
• Path formulae, where g, g1 and g2 are state formulae:
  • `X g`: next
  • `g1 U g2`: until
  • `G g`: globally
  • `F g`: finally
• Next executed event:
  • `EX [e] true`:

Note that these two types of assertions, the LTL and CTL assertions, are not part of the CSP-M language supported by FDR2. Loading a CSP-M file in FDR2 having assertion declarations of this form will exit with a syntax error. Bear in mind to remove or comment out such LTL/CTL assertions in the CSP-M file before loading it in FDR2.

CSP Assertions Viewer

When a CSP-M specification is loaded one can open the CSP Assertion Viewer either from the menu bar of the main window by selecting the `Check CSP-M Assertions` command in the `Verify` menu or from the Refinement button in the ‘’State Properties’’ pane. The viewer looks as follows:

References and Notes