Loading table of contents...
1 Introduction
1.1 Preface
1.2 Organization
2 Getting Started
2.1 Installation
2.2 Graphic User Interface
2.2.1 PAT Editor
2.2.2 PAT Simulator
2.2.3 Graph Difference Analysis
2.2.4 PAT Verifier
2.2.5 New Model Wizard
2.3 System Options
2.3.1 BDD Settings
2.4 LTL to Automata Converter
2.5 Using C# (C/C++/Java) Code as Libraries
2.5.1 External Static Methods
2.5.2 User Defined Data Type
2.5.3 Using Microsoft Contracts.htm
2.5.4 Using C/C++ Code in PAT
2.6 Keyboard Shortcuts
2.7 Command Line
3 Process Analysis Toolkit
3.1 Communicating Sequential Programs (CSP#) module
3.1.1 Language Reference
3.1.1.1 Global Definitions
3.1.1.2 Process Definitions
3.1.1.3 Assertions
3.1.1.4 Expressions
3.1.1.5 Grammar Rules
3.1.1.6 Process Laws
3.1.1.7 Verification Options
3.1.2 CSP Module Tutorial
Bridge Crossing Example
Dining Philosophers Example
Multi-Lift System Example
3.1.3 Miscellaneous
3.2 Real-Time System (RTS) Module
3.2.1 Language Reference
3.2.1.1 Timed Process Definitions
3.2.1.2 Assertions
3.2.1.3 Grammar Rules
3.2.1.4 Verification Options
3.2.2 Real-Time System Tutorial
Fischer's Mutual Exclusion Example
Train Cross Control Example
3.3 Probability CSP (PCSP) Module
3.3.1 Language Reference
3.3.1.1 Probability Processes
3.3.1.2 Assertions
3.3.1.3 Grammar Rules
3.3.1.4 Verification Options
3.3.2 PCSP Module Tutorial
PZ86 Mutual Exclusion
Monty Hall Example
3.4 Probability RTS (PRTS) Module
3.4.1 Language Reference
3.4.1.1 PRTS Processes
3.4.1.2 Assertions
3.4.1.3 Grammar Rules
3.4.2 PRTS Module Tutorial
Multi-lifts System Example
3.5 Labeled Transition System (LTS) Module
3.5.1 Language Reference
3.5.1.1 Global Definitions
3.5.1.2 Primitive Process Definitions
Drawing
Navigation Tree
Canvas
State
Transition
3.5.1.3 Process Definitions
3.5.1.4 Verification Options
3.5.2 LTS Module Tutorial
3.5.2.1 Bridge Crossing Example
3.6 Timed Automata (TA) Module
3.6.1 Language Reference
3.6.1.1 Declarations
3.6.1.2 Process Definitions
Drawing
Navigation Tree
Canvas
State
Transition
3.6.1.3 Grammar Rules
3.6.2 TA Module Tutorial
3.6.2.1 Fischer's Protocol
3.6.2.2 Railway Control System
3.6.2.3 CSMA/CD Protocol
3.7 NesC Module
3.7.1 Language Reference
3.7.1.1 Drawing a Sensor Network
3.7.1.2 The NesC Language
3.7.1.3 TinyOS Library
3.7.1.4 Semantic Model
3.7.1.5 Assertions
3.7.2 nesC Module Tutorial
3.7.2.1 Individual Sensor Tutorial
BlinkApp Example
3.7.2.2 Sensor Network Tutorial
LeaderElection Protocol
3.8 Orc Module
3.8.1 Language Reference.htm
3.8.1.1 The ORC Language.htm
3.8.1.2 Addon for Verification.htm
3.8.1.3 Assertions.htm
3.8.1.4 Supported Sites.htm
3.8.1.5 Grammar Rules.htm
3.8.2 ORC Module Tutorial.htm
3.8.2.1 Metronome.htm
3.8.2.2 Concurrent Quicksort.htm
3.8.2.3 Auction Management.htm
3.9 Stateflow (MDL) Module
3.9.1 Language Reference
3.9.2 Stateflow Tutorial
3.9.2.1 Alarm Monitor
3.9.2.2 Stopwatch
3.9.2.3 Gear Shift
3.9.2.4 Fault-tolerant Fuel Controller
3.9.2.5 SB Logic
3.10 Security Module
3.10.1 Language Reference
3.10.1.1 Specification section
3.10.1.2 Verification section
3.10.1.3 Grammar Rules
3.10.2 SeVe Module Tutorial
3.10.2.1 Needham Schroeder Protocol
3.11 Web Service (WS) Module (obsolete)
3.11.1 Language Reference
3.11.1.1 Global Definitions
3.11.1.2 Web Service Choreography
3.11.1.3 Web Service Orchestration
3.11.1.4 Assertions
3.11.1.5 Grammar Rules
3.11.2 Web Service Tutorial
Online Shopping Example
3.12 UML into PAT
ATM Example
4 Special Features
4.1 Fairness
4.2 Parallel Verification
4.3 Verification of Infinite Systems
4.4 Verification of Linearizability
4.5 Timed Zenoness Checking
5 Developer Guild
5.1 PAT Architecture
5.2 PAT Class Diagram
5.2.1 GUI and Common Package
5.2.2 Module Package
5.3 PAT Extensions
5.3.1 Language Translation
5.3.2 Language Extension
5.3.3 Algorithm Extension
5.3.4 Module Extension
5.3.5 Using PAT as Library
5.4 Module Generator
5.4.1 Module Generation
5.4.2 Working with Generated Code
5.4.3 Example
6 FAQs
Installation FAQ
Using PAT FAQ
7 References
1 Introduction
