The PEP tool provides an integrated development and verification environment for parallel systems. Beginning with version
2.0 it also offers use of timed systems. This paper describes a sample session for the design and the verification by partial
order based techniques of a simple real-time model for a mutual exclusion algorithm.