SATMC Tutorial

This tutorial explains how to use SATMC for model checking an aslan specification within the SPaCIoS Tool. In particular, we will apply SATMC to the ASLan model for the SAML SSO case study.

Prerequisite

Expected results

  • An SATMC output file containing an AAT is created in the workspace.

Tutorial steps

 

    1. Locate the target aslan specification file in the project directory and right-click on it. Locate the SPaCIoS entry inside the contextual menu and move on it. Then, click on “Run SATMC”.
      satmc

 

    1. The SPaCIoS Tool prompts a configuration dialog allowing the user for managing execution settings (see images below). Press button “Ok” to accept default options and proceed.
      satmc
      satmc

 

    1. The SPaCIoS Tool shows a confirmation message presenting the invocation string to the user. Again, press “OK” and continue to the execution.
      satmc

 

    1. The SPaCIoS Tool launches the execution of SATMC and displays the execution progress. When the process terminates, the progress window closes automatically (Note: this step may require several minutes).satmc

 

    1. Move again to the project explorer to check the content of the SPaCIoS project. Find the fresh, new file created by SATMC (this might require to refresh the project view by selecting the SPaCIoS project and pressing F5) named SAML_SSO-SP_init-ACM_2SSLuserlogin.of:

      satmc