PAT: Process Analysis Toolkit

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

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);