VeTeSS-Topcase-Verification-Plugin

Demonstrator for the Topcased VeTeSS plugin.

This readme file gives the instructions necessary for reproducing the experiments made with the Topcased VeTeSS plugin. Additional information can be found in the VeTeSS deliverables.

The demonstrator requires a Windows PC with the following software installed:

• TOPCASED 5.3.0 (http://www.topcased.org)
• PAT 3.4.3 (http://www.comp.nus.edu.sg/~pat/)
• CYGWIN (http://www.cygwin.com/)
• CADP/TGV 2014-j ìAmsterdamî (http://www.inrialpes.fr/vasy/cadp/)

Note that Cygwin is required by CADP/TGV, hence it must be installed before CADP/TGV, by following the instructions in the CADP/TGV web site. It must be installed in the root of the C: disk drive. For CADP/TGV, the default installation location must be selected.

Procedure for installing the plugin:

1. Start Topcased by running its executable file
2. Install the VeTeSS Topcased Verification plugin by the update site. 2.1 Select the Help Install New Software menu item. 2.2 In the Available Software window that appears, copy https://github.com/netgroup-polito/VeTeSS-Topcased-Verification-Plugin/tree/master/update-site and then click on the Add button. 2.3 You will see a Verificationion category with the VeTeSS_TopcasedPluginFeature. Select the most recent version and then click on Finish.
3. Make the plugin visible by selecting Window - Show View - Other and then select Verification
4. In the Settings tab of the plugin view, set the path to the PAT tool.

After having installed the plugin, it is possible to download and open the SysML models of the two use cases (CRF e-shift and airbag):

1. download the zip files of the models from -https://github.com/netgroup-polito/VeTeSS-Topcased-Verification-Plugin/blob/master/models/crf_eshift.zip -https://github.com/netgroup-polito/VeTeSS-Topcased-Verification-Plugin/blob/master/models/ifx_airbag.zip (username: vetess password VeTeSS8765)
2. follow the instructions in the readme.txt file found in each model in order to open it.

In each model it is possible to repeat the refinement checking verifications as follows:

1. in the Verification plugin window select the Refinement checking tab and then click on the Refresh button
2. you should see some requirements already selected. If you want you can modify the selection and then you can click on the Start Verification button in order to start verification.

In each model it is possible to repeat the generation of test cases as follows:

1. in the Verification plugin window select the Test generation tab and then click on the Refresh button
2. you should see some requirements already selected. If you want you can modify the selection.
3. for each selected requirement you can specify the nature of events (input, output or internal). This can be done by clicking on the Scan Gates button: the list of gates (i.e. events) will appear on the right. The nature of events can be changed by acting on the corresponding pull down menu.
4. the test purpose can be automatically gnerated by clicking on the Test purpose generation button.
5. finally, the tests can be generated by clicking on the Test Generation button.
6. the generated tests and other intermediate information can be opened by right clicking on the line of the requirement for which the tests have been generated.