FDR Explorer

In this paper we describe the internal structures of FDR, the refinement model checker for Hoare's Communicating Sequential Processes (CSP), as well as an Application Programming Interface (API) allowing one to interact more closely with, and have fine grained control over, FDR's behaviour and data structures. With such information it is possible to create optimised CSP code to perform refinement checks that are more space/time efficient, hence enabling the analysis of more complex and data intensive specifications. This information is very valuable for both CSP users and tools that automatically generate CSP code, such as those related to security analysis generating test-cases as CSP processes. We also present a simple example of using the tool. Finally, we show how one can transform FDR's graph format into a graph notation (e.g., JGraph), hence enabling visualisation of Labelled Transition Systems (LTS) of CSP specifications.