概要 今後、分散処理システムや並列システムの形態によるアプリケーションの増加 が予想されるが、並列プログラムのデバッグやテストには多大な労力を要する。 そのため、高信頼性の保証されたプログラムを生成するための手段の確立が必要 となる。MENDELS ZONEは、この手段の確立を目指した並列プログラム開発 支援システムであり、種々の形式的手法によって正しい並列プログラムの生成を 支援する。 本論 アプローチ MENDELは、ペトリネットをべ一スとしたKL1の拡張言語であり、KL1に 変換されMulti-PSI上で実行される。そのプログラムは、互いに同期を取りなが ら並列に動作する複数の“オブジェクト"から構成される。MENDELS ZONE は、MENDELの知的プログラミング開発支援システムであり、数学的枠組に基 づいた形式的手法の実装を特徴とする。 従来より、信頼性の高いプログラム開発における形式的手法の有効性が知られ ているが、実用化にあたっては次のような問題があった。MENDELS ZONEでは、オブジェクトの機能を等式論理に基づく代数仕様で、 オブジェクトの動作タイミング仕様を時相論理で記述することにより、(1)の問 題を解決している。また(2)に対しては、形式的手法で記述された仕様の理解性 を高め、かつ記述量を減らすために、ペトリネットなどの図形仕様が併用されて いる。そして、その理解性とモジュラリティの高さから、オブジェクトの部品化 再利用が可能となり、これにより大規模なシステム開発が可能となる。仕様の検 証やプログラムの生成には、等式論理、時相論理の定理証明系を利用している。 これらの定理証明系は、並列実行により処理時間が短縮されており、(4)の問題 の改善が図られている。 以上のアプローチに従い、MENDELS ZONEは形式的手法を実装した。その 結果、仕様の正しさの検証や仕様からプログラムヘの自動変換が可能になり、信 頼性の高いプログラムが生成される。 - 98 -
- 単一の形式的手法によるシステム全体の記述は困難である。
- 仕様の記述量が増えると、形式的記述の理解性が低下する。
- 大規模なシステムの記述に不向きである。
- 仕様の検証やプログラムの生成に多くの時間を要する。