Circus2CSP - A Tool for Model-Checking Circus Using FDR.

In this paper, we introduce Circus2CSP , a tool that automatically translates Circus into CSP M , with an implementation based on a published manual translation scheme. This scheme includes new and modified translation rules that emerged as a result of experimentation. We addressed issues with FDR state-space explosion, by optimising our models using the Circus Refinement Laws. We briefly describe the usage of Circus2CSP along with a discussion of some experiments comparing our tool with the literature.