Currently my main research vehicle is the Moses tool-suite. Moses focuses on the modelling, simulation, implementation, and evaluation/verification of heterogeneous systems using multiple graphical formalisms. Moses originated at the Computer Engineering and Networks Laboratory of the Swiss Federal Institute of Technology.
The Moses web page is a mine of information and the Moses tool-suite can be downloaded from here.
The Adelaide Refinement Checker (ARC) is a Communicating Sequential Processes (CSP) model checking environment. CSP scripts consist of definitions, including those of processes and assertion statements where assertion statements define properties of processes or relationships between processes. With ARC CSP scripts can be edited, parsed, type checked, viewed, checked for data independent types and finally model checked.
The functionality of ARC available here has been restricted to editing, parsing, type checking and exploration of CSP scripts.
