ABSTRACT 

MENDELS ZONE is a software development system for concurrent pro-
grams. The system takes as input several kinds of specifications for MENDEL 
objects, verifies their correctness using automated theorem proving techniques, 
and generates correct KL1 programs semi-automatically. 

KEY FEATURES 

object generation: Specifications, based on equational logic, for MENDEL 
objects are verified in parallel using term rewriting techniques and trans-
formed into MENDEL objects automatically. 
object composition: MENDEL objects are represented by a high-level 
Petri net (MENDEL net). Users compose these objects with the aid of a 
graphical MENDEL net editor. 
object adjustment: Composed objects are automatically adjusted to 
satisfy supplied temporal logic specifications, which specify only timing con-
straints of composed objects. The object adjustment is carried out by parallel 
automated reasoning techniques with Petri nets and temporal logic. 





SYSTEM CONFIGURATION


					- 97 -