概要

MENDELS ZONEは並列プログラムの開発を支援するシステムである。
MENDELオブジェクトの仕様と、オブジェクト間のタイミングに関する制約を
入力すると、定理の自動証明法によってそれらの正しさが検証され、正しいKL1
プログラムが自動生成される。

特徴

オブジェクト生成:等式論理によって記述されたオブジェクトの仕様が、項書
換え技法によって並列に自動検証される。正しさの確認された仕様からは、オブ
ジェクトのプログラム(MENDEL プログラム)が自動生成される。
オブジェクト結合:高レベルペトリネットによって表現されたオブジェクトを、
ユーザが結合する。
オブジェクト調整:タイミングに関する制約を時相論理によって記述する。ペ
トリネットで表されたオブジェクトがその仕様を満たさない場合は、定理証明手
法により仕様を満たすように自動的に調整される。





MENDELS ZONE の構成

					- 97 -