ABSTRACT 

In the future, an increasing number of application programs will be dis-
tributed systems or concurrent systems. Debugging and testing of concurrent 
systems are very difficult, hence it is necessary to establish a methodology for 
the development of reliable programs. MENDELS ZONE is a system whose 
aim is the realization of such a methodology, and supports the development 
of correct concurrent programs through the combined use of several formal 
methods. 

APPROACH 

MENDEL is a concurrent programming language based on Petri net seman-
tics, which can be compiled into KL1 and executed. A MENDEL program is 
composed of several objects which behave concurrently. MENDELS ZONE is 
a concurrent program development system for MENDEL, that adopts formal 
methods based on mathematics. 

Formal methods are recognized as useful in developing reliable programs, 
but the following problems need to be solved before putting them into practical 
use: 
  1. It is difficult to describe a whole system with only one formal method.
  2. Specifications become less comprehensible as their sizes grow larger.
  3. Formal methods are not suitable for large scale systems.
  4. The verification of specifications and the generation of programs are com- putationally costly.
In MENDELS ZONE, the above problems are dealt with as follows. Objects behaviors are described by an algebraic specification based on equational logic, and timing constraints among objects are described using temporal logic. Vi- sual specifications such as Petri nets are used to make formal specifications more understandable and lessen the burden of describing the specifications. Objects can be regarded as reusable parts because of their increased com- prehensibility and modularity, which makes it possible to develop large scale systems. Theorem proving methods for both the equational logic and the tem- poral logic are used in order to verify specifications and transform them into programs. Parallel implementations of these methods contribute in shortening the time necessary for verification and transformation. - 98 -