Other Software

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


Probabilistic Swarm Verifier for BoundeD time properties is a software package for the verification of emergence of bounded time properties in probabilistic swarm systems. Further information can be found in the corresponding paper (published at IJCAI 2018).

Click here to download the source code: PSV-BD