Plug-OBP alias OBP2 is a LTL model-checker for Fiacre models using the OBP compiler providing much more advanded model-checking capabilities. The new version 0.0.4 is out with tons of new features. Verification View

Exploration capabilities

  • Simple Simulation of models
  • Exhaustif BFS, DFS and concurrent BFS explorations,

Executions

  • Pause, resume and stop any exploration,
Idle Execution Idle 1: Start execution
2: Open the simulation view
Running Execution Running 3: Pause execution
4: Stop execution
Paused Execution Paused 5: Resume execution
Done Execution Done 6: Clear results

Model-checking

  • Native Deadlock verification,
  • LTL verification (See the post on GPSL syntax),

Advanced simulation view

  • Configurations presentation:
Tree View Differences Filtering with predicates
Configuration Items Configuration Diffs Configuration Filtering
  • Graph view of visited configuration,
  • Color coding of duplicate configurations,

Simulation View

  • Presentation of counter-example with possibilty to branch.

Counter Example

  • Export of graph views.

Export

  • The trace view is a simple and light view that will be opened instead of the graph view if the counter example contains more than 1500 nodes. It also can be enforced if shift is pressed when opening the graph view.

Trace