Insight

Insight

The Insight tool is designed for the analysis of invariants that have been automatically generated by the Specstractor framework. Insight offers the user high level views on the resulting invariants in the form of state machines and visualizations and allows for searching, filtering and comparison of invariants.

The tool can be accessed here. The link will bring you to the start page of the insight tool from which you can load a set of three example invariants from the automotive and medical device domain that are distributed with the tool. For more information about the specific system click on tell me more under the short description.

Tutorial

Please press the load button of the cruise control example now. A popup on the bottom of the screen will inform you if the data has been loaded successfully (be aware that any data that is already loaded will be removed and replaced by the cruise control example data).

Inspecting the Invariants

On the left side you can see the navigation panel. From which you can access all features of the Insight tool. Let’s start by going to the Property Screen (click on Properties in the navigation list on the left). This will bring up the property viewer that shows you all the currently loaded invariants.

To filter invariants you can click on the name of any of the variables in the invariants Insight will then only show invariants that contain the selected variables. The same can be done by clicking on the value of one of the variables then it will only show invariants that contain variables with the selected values.

To remove the filters press the X button on the top right of the page.

State Machine Creator

Insight can create State Machine views for systems if the invariants contain internal state variables of the system. In case that you have not done so yet, please load the cruise control example. Then click on the State Machine link on the navigation pane on the left. This will open the configuration screen of the state machine creator.

The internal variable of the cruise control system is mode and the variable that observes the previous timestep of mode is oldMode. On the top of the configuration screen please select mode and oldmode and then press add Variables. The selected variables will appear below and you can now press Create Statechart. This will close the configuration screen and the state machine will appear.

For systems that have more than one internal variable you can choose several pairs of internal variables to observe.

Impact Score

The Impact score shows how often an input or internal variable is involved in an invariant for a specific output variable. The results are visualized in a heat map that you can access under Charts on the navigation panel. Hovering over one of the quadrants of the heat map will show you its impact score. Clicking on a quadrant of the heat map will bring up the property viewer screen that shows you all the invariants of the chosen quadrant.

Loading your own Invariants

You can also load text files created by the [Extractor]. To do so click on Data in the navigation screen. Which will bring up the data management screen. Here you can click the Choose File button to chose an invariant file from your filesystem, after choosing the file its name should show up next to the button. By clicking on Load below the Choose File button the file is loaded and its invariants are added into Insight and the file will appear below in Data Files. In Data Files you can manage all files that you uploaded, you can deactivate them or remove them alltogether.

Comparing two sets of Invariants

On the data screen you can also compare two sets of invariants against each other. Please load the Heart Model example from the Home page then return back to the Data page. As you can see there are two files loaded now path1.txt and path2.txt.

On the bottom of the Data page, under File Comparison you can choose the invariant files you would like to compare against each other. Please select path1 and path2 here and then click on Compare Files.

This will load the comparison screen, which is a variant of the properties screen. On top you have a three tabs, the first tab shows all invariants that are in both path1 and path2. The second tab shows all invariants in path1 and the third tab all in path2.