図 2



多くの場合、オブジェクト内のメソッド間、あるいはオブジェクト間には、そ
の起動順序に何らかの制約を必要とする。このとき、ユーザはにその順序制
約を時相論理で記述する。MENDELS ZONEは、定理証明手続きタブロー法を
用いて、その制約を満たすようにペトリネットの自動調整を行なう。ここでいう
調整とは、プログラム制御用のアービターの生成を意味する。完成した
MENDELプログラムは、KL1プログラムにコンパイルされる。生成されたKL1
プログラムの実行は、MENDELS ZONEでグラフィカルにモニタできる。

			成果

並列システム開発でのMENDELS ZONEの有用性を評価するため、発電所制
御エキスパートシステムの開発を行なった。このシステムは、先に直接KL1で開
発されており、今回はそれと同機能のシステムをMENDELS ZONE上で開発し
た。これにより、MENDELS ZONEによって実システムが充分構築できること
が確認された。また両者を比較すると、MENDELS ZONEによる開発ではコー
ディングに時間がかかるもののデバッグ時間はかなり短縮された。このことは、
形式的手法による検証機能の有用性を示している。

デモ概要

デモでは、MENDELS ZONEの機能を、発電所制御エキスパートシステムの
開発例を用いて説明する。あわせて、この開発事例を某にしたMENDELS ZONE
の評価を示す。


					- 100 -