To trigger verification of the current drawing, select menu "SCStudio – Verify", or click the Verify toolbar button, or press Ctrl+Alt+C.
The SCStudio verifies the drawing, including all charts referenced from that drawing (see MSC Reference).

This SCStudio version is able to check the following properties:

  • Acyclic (in basic MSC only)
  • FIFO (in basic MSC only)
  • Deadlock Free (in HMSC only)
  • Livelock Free (in HMSC only)
  • Race Free (in both basic MSC and HMSC)
  • Universal Boundedness (in HMSC only)
  • Local Choice (in HMSC only)
  • Strong Realizability (both in basic MSC and HMSC)
  • Time Consistency (in both basic MSC and HMSC)
  • Time Race (in both basic MSC and HMSC)

Verification Report

Errors and warnings will be listed in a “Verification Report”. Some lines in the report may include hypertext links. If you click such a link in the report, related shapes in your drawing will be selected. This may help you to locate the error.

Counterexample
Errors generated by verification algorithms will display an example that violates the verified property. These examples are displayed in a new document. Each counterexample shows portions of the original drawing, having erroneous parts highlighted.The original document remains unchanged.
The following figure shows a sample MSC and a respective counterexample for a race condition (meaning the messages might come in a different order than anticipated).

Options

Verification can be configured in the Verification Settings dialog invoked by the “SCStudio – Options...” menu.