Verification View: Difference between revisions

No edit summary
 
(3 intermediate revisions by the same user not shown)
Line 3: Line 3:
*LTL Verifications and
*LTL Verifications and
*Constraint Based Checking
*Constraint Based Checking
In each tab you can add multiple tests to check you currently selected machine.
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==
==Modelchecking==
[[File:Modelchecking.png|left]]
[[File:Modelchecking.png|left]]
By pressing the plus button you can add several model checking variants. The following view will be shown:
[[File:Modelchecking Stage.png|left]]
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==
==LTL Verifications==
[[File:LTL.png|left]]
[[File:LTL.png|left]]
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.
==Constraint Based Checking==
==Constraint Based Checking==
[[File:CBC.png|left]]
[[File:CBC.png|left]]
[[File:Add CBC.png|left]]

Latest revision as of 07:49, 11 October 2017

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

  • Modelchecking
  • LTL Verifications and
  • Constraint Based 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

Modelchecking.png

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

Modelchecking Stage.png

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

LTL.png

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.

Constraint Based Checking

CBC.png
Add CBC.png