Tyger: A Tool for Automatically Simulating CSP−Like Languages in CSP
Thomas Gibson−Robinson · 2010
In [Ros08b] Roscoe outlines a class of languages, termed CSP-like languages, that can be simulated within CSP. Furthermore, Roscoe provides a construction that, given the operational semantics of an operator, gives a CSP simulation of the operator that is strongly bisimilar to the original operator. However, the construction is difficult to use, both for specifying the operational semantics and the processes that the user wishes to simulate. Furthermore, the construction is unfortunately infinite state even when simple recursive processes are used and therefore the construction is unable to be compiled by the CSP model checker, FDR. In this Thesis we aim to solve both of these problems by, firstly, giving an adaptation to the construction that enables recursion to be successfully compiled by FDR. We then give many optimisations to the simulation to enable it to run at a reasonable speed through FDR. Lastly, we introduce Tyger, a Haskell program that is able to automate the construction of the simulation given a specification of the operational semantics of a language. Furthermore Tyger allows a user to supply process definitions using custom infix operators meaning that process definitions can be input and read easily. Lastly, Tyger also implements a type checker for the functional language that it uses meaning that many errors that would result in esoteric runtime errors in FDR can be caught at compile time. ii