Editing Communicating sequential processes (section)

== Tools ==
Over the years, a number of tools for analyzing and understanding systems described using CSP have been produced. Early tool implementations used a variety of machine-readable syntaxes for CSP, making input files written for different tools incompatible. However, most CSP tools have now standardized on the machine-readable dialect of CSP devised by Bryan Scattergood, sometimes referred to as CSP<sub>''M''</sub>.<ref>{{Cite thesis |last=Scattergood |first=J. B. |title=The Semantics and Implementation of Machine-Readable CSP |type=[[D.Phil.]] |publisher=[[Oxford University Computing Laboratory]] |date=1998}}</ref> The CSP<sub>''M''</sub> dialect of CSP possesses a formally defined [[operational semantics]], which includes an embedded [[functional programming language]].

=== FDR ===

The most well-known CSP tool is probably ''[[FDR (software)|Failures-Divergences Refinement]]'', which is a commercial product originally developed by Formal Systems (Europe) Ltd. FDR is often described as a [[model checker]], but is technically a ''refinement'' checker, in that it converts two CSP process expressions into [[Labelled transition system|Labelled Transition Systems]] (LTSs), and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, or failures/divergence).<ref>{{Cite book |first=A. W. |last=Roscoe |chapter=Model-checking CSP |title=A Classical Mind: Essays in Honour of C. A. R. Hoare |publisher=Prentice Hall |date=1994 |author-link=Bill Roscoe}}</ref> FDR applies various state-space compression algorithms to the process LTSs in order to reduce the size of the state-space that must be explored during a refinement check. FDR was succeeded by FDR2, FDR3 and FDR4.<ref>{{cite web |url= https://www.cs.ox.ac.uk/projects/fdr/manual/introduction.html |title=Introduction — FDR 4.2.4 documentation |website=www.cs.ox.ac.uk}}</ref>

=== ARC ===

The ''Adelaide Refinement Checker'' (''ARC'')<ref>{{cite conference |first1=Atanas N. |last1=Parashkevov |first2=Jay |last2=Yantchev |title=ARC – a tool for efficient refinement and equivalence checking for CSP |book-title=IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96 |pages=68–75 |date=1996 |citeseerx=10.1.1.45.3212}}</ref> is a CSP refinement checker developed by the Formal Modelling and Verification Group at [[The University of Adelaide]]. ARC differs from FDR2 in that it internally represents CSP processes as [[Binary decision diagram|Ordered Binary Decision Diagrams]] (OBDDs), which alleviates the state explosion problem of explicit LTS representations without requiring the use of state-space compression algorithms such as those used in FDR2.

=== ProB ===

The ''ProB'' project,<ref>{{cite conference |first1=Michael |last1=Leuschel |first2=Marc |last2=Fontaine |title=Probing the Depths of CSP-M: A new FDR-compliant Validation Tool |book-title=ICFEM 2008 |publisher=Springer-Verlag |date=2008 |url= http://www.stups.uni-duesseldorf.de/publications/main.pdf |access-date=2008-11-26 |url-status=dead |archive-url= https://web.archive.org/web/20110719102153/http://www.stups.uni-duesseldorf.de/publications/main.pdf |archive-date=2011-07-19}}</ref> which is hosted by the Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, was originally created to support analysis of specifications constructed in the [[B method]]. However, it also includes support for analysis of CSP processes both through refinement checking, and [[Linear Temporal Logic|LTL]] model-checking. ProB can also be used to verify properties of combined CSP and B specifications. A ProBE CSP Animator is integrated in FDR3.

=== PAT ===

The ''Process Analysis Toolkit'' (PAT)
<ref>{{cite conference |last1=Sun |first1=Jun |first2=Yang |last2=Liu |first3=Jin Song |last3=Dong |title=PAT: Towards Flexible Verification under Fairness |book-title=Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009) |publisher=Springer |series=Lecture Notes in Computer Science |volume=5643 |date=2009 |url= http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf |access-date=2009-06-16 |url-status=dead |archive-url= https://web.archive.org/web/20110611055744/http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf |archive-date=2011-06-11}}</ref><ref>{{cite conference |last1=Sun |first1=Jun |first2=Yang |last2=Liu |first3=Jin Song |last3=Dong |title=Model Checking CSP Revisited: Introducing a Process Analysis Toolkit |book-title=Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008) |pages=307–322 |publisher=Springer |series=Communications in Computer and Information Science |volume=17 |date=2008 |url= http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf |access-date=2009-01-15 |url-status=dead |archive-url= https://web.archive.org/web/20090108091954/http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf |archive-date=2009-01-08}}</ref> is a CSP analysis tool developed in the School of Computing at the [[National University of Singapore]]. PAT is able to perform refinement checking, LTL model-checking, and simulation of CSP and Timed CSP processes. The PAT process language extends CSP with support for mutable shared variables, asynchronous message passing, and a variety of fairness and quantitative time related process constructs such as <code>deadline</code> and <code>waituntil</code>. The underlying design principle of the PAT process language is to combine a high-level specification language with procedural programs (e.g. an event in PAT may be a sequential program or even an external C# library call) for greater expressiveness. Mutable shared variables and asynchronous channels provide a convenient [[syntactic sugar]] for well-known process modelling patterns used in standard CSP. The PAT syntax is similar, but not identical, to CSP<sub>''M''</sub>.<ref>{{cite conference |first1=Jun |last1=Sun |first2=Yang |last2=Liu |first3=Jin Song |last3=Dong |first4=Chunqing |last4=Chen |title=Integrating Specifications and Programs for System Specification and Verification |book-title=IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09 |date=2009 |url= http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf |access-date=2009-04-13 |url-status=dead |archive-url= https://web.archive.org/web/20110611055219/http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf |archive-date=2011-06-11}}</ref> The principal differences between the PAT syntax and standard CSP<sub>''M''</sub> are the use of semicolons to terminate process expressions, the inclusion of syntactic sugar for variables and assignments, and the use of slightly different syntax for internal choice and parallel composition.

=== Others ===

''VisualNets''<ref>{{cite conference |last1=Green |first1=Mark |first2=Ali |last2=Abdallah |title=Performance Analysis and Behaviour Tuning for Optimisation of Communicating Systems |book-title=Communicating Process Architectures 2002 |date=2002 |url= https://www.researchgate.net/publication/290383042}}</ref> produces animated visualisations of CSP systems from specifications, and supports timed CSP.

''CSPsim''<ref>{{cite conference |last1=Brooke |first1=Phillip |first2=Richard |last2=Paige |title=Lazy Exploration and Checking of CSP Models with CSPsim |book-title=Communicating Process Architectures 2007 |date=2007}}</ref> is a lazy simulator.  It does not model check CSP, but is useful for exploring very large (potentially infinite) systems.

[http://www.principia-m.com/syncstitch/ SyncStitch]  is a CSP refinement checker with interactive modeling and analyzing environment. It has a graphical state-transition diagram editor. The user can model the behavior of processes as not only CSP expressions but also state-transition diagrams. The result of checking are also reported graphically as computation-trees and can be analyzed interactively with peripheral inspecting tools. In addition to refinement checks, It can perform deadlock check and livelock check.