In LOTOS, requirements for a distributed system are described as a service definition. On the protocol level, each node (protocol entity) must exchange some data values and synchronization messages to provide a service described in a service definition. The tuple of the specifications of all nodes in the system which provide the service is called as a protocol specification. In order to develop the communication programs satisfying a given service definition, it is very important to develop the correct protocol specification. For this purpose, the simulation of protocol specifications is useful and it is desirable that the designer can observe how a protocol specification is executed in parallel and how synchronization messages are exchanged among the nodes. Therefore, we have developed a new tool named PROSPEX. For a given pair of a service definition and a protocol specification, it executes the protocol specification in parallel and shows its execution process graphically on X Window System. If the protocol specification executes an event sequence which does not satisfy the service definition, then PROSPEX informs it to the designer. In this paper, the design and usefulness of PROSPEX are described.