ISPL Fault Injector is a generic compiler for automatically injecting faults into an ISPL program.
There is also an example of a protocol available to download.
The protocol contains the following faults:
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.
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).