PROSPEX: A Graphical LOTOS Simulator for Protocol Specifications with N Nodes

Keiichi YASUMOTO  Teruo HIGASHINO  Toshio MATSUURA  Kenichi TANIGUCHI  

Publication
IEICE TRANSACTIONS on Communications   Vol.E75-B   No.10   pp.1015-1023
Publication Date: 1992/10/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8516
Type of Manuscript: Special Section PAPER (Special Issue on Communication Software Technologies)
Category: 
Keyword: 
LOTOS,  service definition,  protocol specification,  simulator,  correctness,  

Full Text: PDF>>
Buy this Article




Summary: 
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.