IBT Tutorial

This tutorial explain how to use the IBT tool. As a running example we use the SAML SSO security protocol example.


Expected results

  • Concretize and execute an abstract test case.

Resources required

Tutorial steps


    1. Create an account: Register an account on Feide OpenIdP, if you do not have one yet:
      1. Access here and follow the registration process.
      2. Please take note of your username and password. In the sequel, we will refer to them as (USR) and (PWD) respectively.


    1. Download and unzip the project: Download and unzip the file SAML2-SSO.zip:
      1. (P1): the SAML2-SSO SPaCIoS project: ASLan++, ASLan, OF, IUT files and others.
      2. (P2): the SpaciosHTTPHTMLAdapters Java project: common testing adapter for HTTP and HTML.

      Notice that project (P1) depends on project (P2).


    1. Run Eclipse with the SPaCIoS Tool and import the projects:
        1. Run your Eclipse with the SPaCIoS Tool.
        2. Import the projects (P1) and (P2) following the these steps:





    1. Set the testing user and password:
        1. Open the class saml_sso.setup.FoodlXfeideSetup within theSAML2-SSO project. See figure below.
        2. Set the strings to the (USR) and (PWD), first step of the tutorial.



    1. Open the abstract trace (optional):
      1. Open the abstract trace saml_sso-sp_init-acm_2ssluserlogin-functional.of
      2. Click on the “Events Sequence Chart” tab to see the graphical view of the abstract trace
      3. Click on the “\#” button of the Outline to see the list of steps of the abstract trace

      You should obtain an output similar to the image below. This abstract trace captures the functional execution of the protocol. It has been obtained by model-checking the file SAML_SSO-SP_init-ACM_2SSLuserlogin-functional.aslanautomatically generated from its ASLan++ specification.


    1. Open the IUT (optional): Open the IUT file foodlXfeide.iut:


    1. Create the “Execute Abstract Trace” run configuration:
      1. Open the run configuration:
      2. Go to the “Execute Abstract Trace”
      3. Create a new launch configuration,
      4. Fill-in as the figure below. Set the proxy if and only if you are behind a proxy.


  1. Execute the testcase:
    1. Click on the run button of the run configuration you just created.
    2. You may get an pop-up. In case just click on yes.
    3. You should see the console printing out many logging information.
    4. The “Test Execution Result” view should open.
    5. Double-click on the last line and then click on the “Browser rendering” tab. You should get something similar to:
    6. You should get a SUCCESS verdict in the console: