Model checking using iSpin on Windows

Ever tried to do model verification using iSpin (on Windows) on a click of a button but couldn’t manage to get it to work? I had the same problem. Apparently, there aren’t good resources that solve this problem. Follow these steps to get it to work. This has been tested to work on Widnows 7 and Windows 8.

I assume you have iSpin and SPIN installed on you system. Now let’s proceed with the necessary components. While doing the command line verification, most probably you used Cygwin’s gcc. or if you haven’t done any model verification so far, please first download and install Cygwin (note that you can also use MinGW instead of Cygwin – but this solution works for both). Then download and install gcc – C, C++ compiler package. When the installation completes, click on the Start menu, then right click on Computer and click on Properties. On the left navigation, click on Advanced system settings — a dialog will appear. On the dialog, click on Environmental Variables. Now a new dialog will open. Under the System variables section, locate the variable Path, select it and click on Edit. At the end of Variable value, add semi-colon (;) and add the path where you installed Cygwin plus Bin folder. That is, if you installed Cygwin in C:\Cygwin, then add the following


If you’re using the MinGW version of gcc rather than Cygwin, use instead the following (assuming MinGW is installed in C:\MinGW\)


and click on OK. Then click on OK on the previous dialogs.

Now, navigate to the path where you installed SPIN. Locate iSpin, then open it in a text editor (I used Notepad++). Now locate the line that reads the following:

set CC      gcc

Add the following line just under it (select the one that applies for you)

set CC      “C:/Cygwin/bin/gcc”          ; for Cygwin users

set CC      “C:/MinGW/bin/gcc”          ; for MinGW users

That’s it. Save the file and close it. Now as a test, open iSpin and then open some model. Then write the LTL properties you want to verify inside the model, save it, and reopen it. Then go to the verification tab and adjust the commands to be used as per your requirements. Then click on the Run button. After some time, you should see the result on the Verification result window (the dark windows on the right bottom).


Installing WebGoat on Windows

Recently, I had to work on WebGoat to study the possible vulnerabilities we can have on a test web application. But since I used to normally work on Windows (Linux now), installing it and having it to start to work was a bit tiresome. After a while, I managed to install everything needed. So here are the steps I followed to get it work.

You need to have Java and Tomcat installed on your system. Assuming Java will be there, you can download Tomcat from here. Install Tomcat in the root folder instead of the Program Files folder to avoid messing with the permission settings. When the installation finishes, go to the installation directory and navigate to the conf folder and open tomcat-users.xml file. Under <tomcat-users> tag, insert the following text

<role rolename=”admin-gui”/>
<role rolename=”manager-gui”/>

<role rolename=”webgoat_admin”/>
<role rolename=”webgoat_user”/>
<role rolename=”webgoat_basic”/>

<user name=”webgoat” password=”webgoat” roles=”webgoat_admin” />
<user name=”guest” password=”guest” roles=”webgoat_user” />
<user name=”basic” password=”basic” roles=”webgoat_basic” />
<user name=”admin” password=”yourpassword” roles=”admin-gui,manager-gui” />

Now download the latest version of WebGoat WAR file from here. At this time, Tomcat should be listening on http://localhost:8080 unless you modified this setting during the installation of Tomcat. Open that address on your browser. Click on Manage App and then insert the username and password you specified at the last line of the above code. Then go down to WAR file to deploy section and locate your installation file from your download folder and click on Deploy.

That’s it. Now you should be able to see the WebGoat app working by navigating to http://localhost:8080/WebGoat/attack.