Editing Communicating sequential processes (section)

=== 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.