-
User Manual
The user manual is available online.
The CHM version can be downloaded HERE.
The PDF version can be downloaded HERE.If you are interested in the technical details of PAT, refer to our Publications.
API for PAT.Common.dll
The CHM version can be downloaded HERE.
This file include all methods and fields for PAT.Common project. All module needs to follow these APIs in order to be recongnized by PAT framework.
Please refer to user manual on how to use the APIs to develop custimized module in PAT.Documantation and Tutorials of PAT
1 PAT Getting Started-1 PAT Getting Started-2 (Power Point). A starting guild of how to use PAT. Some simple syntax examples are here.
2 CSP Slides (PDF). CSP introduction lecture notes.
3 CSP Semantics 1, CSP Semantics 1 (PDF). CSP Semantics Introduction lecture notes.
4 PAT Presentation (Power Point). Slides for PAT Talks, including fairness definitions and refinement checking.
5 Model Checking. Slides for a general introduction to Model Checking.
6 PAT Advanced Topics (Power Point). The peterson’s algorithm can be download here
7 PAT Presentation Slides on ICFEM 08 (Power Point).
8 PAT Presentation Slides on CAV 09 about fairness.
9 PAT Input Language CSP# Slides on TASE 09 (Power Point).
10 Verify Population Protocol Slides on TASE 09 (Power Point).
11 Towards Expressive Specification and Efficient Model Checking Slides on TASE 09 (Power Point).
12 Model Checking Lineariability via Refinement Slides on FM 09 (Power Point).
13 Fair Model Checking of Parameterized Systems Slides on FM 09 (Power Point). -
Video
We are making short videos for PAT basing modules. More videos are coming
PCSP Module: AVI Format youtube Contributed by Song SongZheng
NESC Module: AVI Format youtube Contributed by Zheng ManChun -
Experiments
Experiments results in PAT are categorized by modules.
The test bed’s configuration is as follows:
- Intel Xeon 4-Core CPU*2, 32 GB memory and 6 TB Hard Disk.
- Windows Server 2008 64 Bit
- PAT Version 3.2
CSP Module
RTS Module
PCSP Module
PRTS Module
TA Module
NesC Module