5デモ概要
モチーフの摘出条件を設定し、PIM上で実際にモチーフ抽出実験を行なう。
モチーフ抽出の実行中には、PIM上の各プロセッサ上に存在するモチーフ候補
の記述長が時間とともに減少していく様子を、モザイク状のカラー表示と折れ線
グラフ表示でリアルタイムに示す。モチーフ抽出の結果は、確率約決定述語の形
で表示する。この際、抽出されたモチーフのアミノ酸配列上での位置、タンパク
質の立体構造中での位置も合わせて表示する。モチーフ抽出の途中経過と抽出結
果の画面例を以下に示す。
MENDELS ZONE
並列プログラム開発支援システム
概要
MENDELS ZONEは並列プログラムの開発を支援するシステムである。
MENDELオブジェクトの仕様と、オブジェクト間のタイミングに関する制約を
入力すると、定理の自動証明法によってそれらの正しさが検証され、正しいKL1
プログラムが自動生成される。
特徴
●オブジェクト生成:等式論理によって記述されたオブジェクトの仕様が、項書
換え技法によって並列に自動検証される。正しさの確認された仕様からは、オブ
ジェクトのプログラム(MENDEL プログラム)が自動生成される。
●オブジェクト結合:高レベルペトリネットによって表現されたオブジェクトを、
ユーザが結合する。
●オブジェクト調整:タイミングに関する制約を時相論理によって記述する。ペ
トリネットで表されたオブジェクトがその仕様を満たさない場合は、定理証明手
法により仕様を満たすように自動的に調整される。
概要
今後、分散処理システムや並列システムの形態によるアプリケーションの増加
が予想されるが、並列プログラムのデバッグやテストには多大な労力を要する。
そのため、高信頼性の保証されたプログラムを生成するための手段の確立が必要
となる。MENDELS ZONEは、この手段の確立を目指した並列プログラム開発
支援システムであり、種々の形式的手法によって正しい並列プログラムの生成を
支援する。
本論
アプローチ
MENDELは、ペトリネットをべ一スとしたKL1の拡張言語であり、KL1に
変換されMulti-PSI上で実行される。そのプログラムは、互いに同期を取りなが
ら並列に動作する複数の“オブジェクト"から構成される。MENDELS ZONE
は、MENDELの知的プログラミング開発支援システムであり、数学的枠組に基
づいた形式的手法の実装を特徴とする。
従来より、信頼性の高いプログラム開発における形式的手法の有効性が知られ
ているが、実用化にあたっては次のような問題があった。
1.単一の形式的手法によるシステム全体の記述は困難である。
2.仕様の記述量が増えると、形式的記述の理解性が低下する。
3.大規模なシステムの記述に不向きである。
4.仕様の検証やプログラムの生成に多くの時間を要する。
MENDELS ZONEでは、オブジェクトの機能を等式論理に基づく代数仕様で、
オブジェクトの動作タイミング仕様を時相論理で記述することにより、(1)の問
題を解決している。また(2)に対しては、形式的手法で記述された仕様の理解性
を高め、かつ記述量を減らすために、ペトリネットなどの図形仕様が併用されて
いる。そして、その理解性とモジュラリティの高さから、オブジェクトの部品化
再利用が可能となり、これにより大規模なシステム開発が可能となる。仕様の検
証やプログラムの生成には、等式論理、時相論理の定理証明系を利用している。
これらの定理証明系は、並列実行により処理時間が短縮されており、(4)の問題
の改善が図られている。
以上のアプローチに従い、MENDELS ZONEは形式的手法を実装した。その
結果、仕様の正しさの検証や仕様からプログラムヘの自動変換が可能になり、信
頼性の高いプログラムが生成される。
システムの概要
MENDELS ZONE上の開発は、オブジェクトを生成する“代数仕様フェーズ”と
オブジェクトを結合する“ペトリネットフェーズ”に分けられる。
ユーザは、オブジェクトの機能(メソッド)を代数的仕様記述で与える。正
しい仕様を記述するために、MENDELS ZONEは、仕様の文法チェック、項書
換えとしての直接実行、潜在帰納法による検証などの支援を行なう。ユーザは、
より仕様の満たすべき検証項目を入力すると、MENDELS ZONEは仕様がその
検証項目を満たしているかどうかを自動検証し、で検証手続きの進行状況が
確認できる。正しさが確認されたら、MENDELオブジェクトヘ自動変換を行な
う。
図2にペトリネットフェーズの画面イメージを示す。
自動変換で生成されたオブジェクトは、の部品ライブラリに登録される。オ
ブジェクトの結合は高レベルペトリネットで表現することができ、その記述は
のペトリネットエディタでマウス操作のみで行なえる。
多くの場合、オブジェクト内のメソッド間、あるいはオブジェクト間には、そ
の起動順序に何らかの制約を必要とする。このとき、ユーザはにその順序制
約を時相論理で記述する。MENDELS ZONEは、定理証明手続きタブロー法を
用いて、その制約を満たすようにペトリネットの自動調整を行なう。ここでいう
調整とは、プログラム制御用のアービターの生成を意味する。完成した
MENDELプログラムは、KL1プログラムにコンパイルされる。生成されたKL1
プログラムの実行は、MENDELS ZONEでグラフィカルにモニタできる。
成果
並列システム開発でのMENDELS ZONEの有用性を評価するため、発電所制
御エキスパートシステムの開発を行なった。このシステムは、先に直接KL1で開
発されており、今回はそれと同機能のシステムをMENDELS ZONE上で開発し
た。これにより、MENDELS ZONEによって実システムが充分構築できること
が確認された。また両者を比較すると、MENDELS ZONEによる開発ではコー
ディングに時間がかかるもののデバッグ時間はかなり短縮された。このことは、
形式的手法による検証機能の有用性を示している。
デモ概要
デモでは、MENDELS ZONEの機能を、発電所制御エキスパートシステムの
開発例を用いて説明する。あわせて、この開発事例を某にしたMENDELS ZONE
の評価を示す。