a object or among objects. In such a case, users denote the timing constraints 
using temporal logic . MENDELS ZONE adjusts Petri nets automatically in 
order to satisfy the constraints. This program adjustment means synthesizing 
an arbiter that is attached to the original programs. A completed MENDEL 
program is compiled into a KL1 program, whose execution can be monitored 
within the environment provided by MENDELS ZONE. 




FIGURE 2


RESULT 

We have developed an control system of a power station in order to exam-
ine the effectiveness of MENDELS ZONE for the development of a concurrent 
system. This control system was originally implemented directly in KL1, and 
we developed an almost identical system using MENDELS ZONE. Based on 
this experience, we feel confident in saying that a real system can be developed 
using MENDELS ZONE. A comparison between two development efforts re-
veals that MENDELS ZONE reduces debugging time although more time is 
needed for specifying and coding. This fact is an indication of effectiveness of 
verification based on formal methods. 

OUTLINE OF DEMONSTRATION 

We demonstrate the capabilities of MENDELS ZONE using the develop-
ment example of the control system, and show the result of this development. 


					- 100 -