Using ITS modeler to analyze ITS systems.

The ITS Modeler front-end for its-tools can be used to analyze models built using ITS Modeler with the its-tools.

I. Install

II. Analyzing models

1. Reachability

To analyze models, we first need to create an ITS adapter that will wrap the Time Petri nets into instantiable transition systems.

Create a "File->New->Other->Coloane->ITS Composition model", Next, give it a name, Finish.

From the explorer on the left drag and drop the model(s) you wish to analyze into the "Types Declaration" frame (you can use multi selection). Then specify the various parameter bindings (variables of TPN models, type bindings of composite ITS models) as explained above.

Finally, select the model you want to analyze (usually the top-level model, with an empty offered interface, the full system composition), then click the "Analysis" button, which will setup a new tab in the same pane (switch between tabs at bottom of window).

You can now use the ITS reach service for instance: select "ITS reachability" then "Run Service"

You should get a service report that indicates some statistics on number of reachable states.

2. CTL

For the CTL service, I'll use examples from the Fischer example. You can get this model by "File->New->Example->Coloane->Fischer's Mutual exclusion" .

In the analysis tab, select "CTL check" "then "Add a formula"

Write a CTL formula, then select "Run service" you will obtain true/false results for your formulas.