PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

Monthly archives for October, 2007

Readers-Writers Problem

The readers/writers problem describes a protocol for coordination of N readers and N writers accessing a shared resource.

The CSP definition of Readers-Writers Problem of size N is defined as follows.




The property to verify is reachability of an erroneous situation (i.e., wrong readers/writers coordination).
[]<>error

The following defintion is the MS example with size 2.
====================Process Definitions====================
Reading0()=Controller;
Reading1()=((startread->Reading2)[](stopread->Reading0));
Reading2()=(stopread->Reading1);
Writing()=((stopwrite->Controller)[](stopread->(error->Writing)));

Writer0()=(startwrite->(stopwrite->Writer0));
Writer1()=(startwrite->(stopwrite->Writer1));

Reader1()=(startread->(stopread->Reader1));
Reader0()=(startread->(stopread->Reader0));

Controller()=((startread->Reading1)[]((stopread->(error->Controller))[](startwrite->Writing)));
aReadersWriters()=(Controller||(Reader0|||Reader1)||(Writer0|||Writer1));

============================LTL Definitions============================
LTL(AlwaysError=[]<>error);

Model Checkers

We have implemented both explicit model checking as well as bounded model checking for systematic analysis of CSP models. In our implementation, there is 2 model checkers are implemented:

  • On-the-fly model checking: to verify the CSP processes with or without fair events.
  • Bounded model checking: to verify the CSP processes without fair events based on the SAT Solvers.

The details of the two model checkers are in the submitted publications.

CSP Simulator

CSP simulator takes in the specifications and allows users to perform various simulation tasks:

  • Complete states generation based on the execution graph. The generation may not terminate if the states are not finite.
  • Automatically Random Simulation with animation
  • User interactive simulation with Step by Step execution
  • Trace display and replay

Specification Editor

Specification editor accepts the CSP specifications and LTL properties defined in How to write Process Definitions and How to write LTL Formulae respectively.

Specification editor has an extremely user friendly user interface with following features:

  • Complete text editing functions
  • Syntax highlighting
  • Multi-threading execution
  • Multi-documents environment

Screen Shots

PAT

PAT

Simulator

Simulator

Buchi Automata Viewer

BAViewer

Model Checker

Model Checker