Other Software

This page lists a few miscelleanous software packages produced by our group.

ISPL Fault Injector

ISPL Fault Injector is a generic compiler for automatically injecting faults into an ISPL program.

Click here to download the source code: ISPL Fault Injector

There is also an example of a protocol available to download.

Click here to download the ISPL program for the token ring protocol with faults

The protocol contains the following faults:

  • TKwd: a populated data token becomes destined for the wrong workstation.
  • N1sm: node 1 becomes a standby monitor if it is an active monitor.
  • sN2ns: node 2 stops sending tokens.
  • hN3ns: node 3 stops sending tokens.
  • hN4nr: node 4 stops receiving tokens.
  • hN6ns: node 6 stops sending tokens.


GSMC is an experimental model checker for GSM, the Guard-Stage-Milestone language for programming artifact-centric systems. GSMC uses predicate abstraction techniques and is integrated with CVC4, one of the leading SMT solvers. GSMC is released as open-source and is developed as part of the ACSI (Artifact-centric Service Interoperations) EU FP7 research project.

Click here to download the source code: GSMC