[ トップページ ]
現代の社会は大規模で高度なソフトウェアによって支えられており，今後の社会の進展やIT化などによりそのようなソフトウェアに対する要求が益々強くなってくると思われます． しかしながら，現在このようなソフトウェアを効率良くかつ確実に開発し，進化・発展させるための技術が十分には確立されてはいません． この理由のひとつに，現在のソフトウェア開発技術が，十分な科学的な基盤の上に展開されておらず，計算機科学の最新の研究成果をとり入れることが出来ていないことがあげられます． このような立場から，本プロジェクトでは科学的・形式的手法にもとづくソフトウェア開発方法論を，
の4つの課題に焦点をあてて研究を行なってきました．
片山グループでは，科学的方法によってソフトウェアを開発し，また，開発されたソフトウェアを合理的に発展させるための発展的ソフトウェア開発方法論について，独創的な研究を行なってきました．
オブジェクト指向開発方法論は，発展的ソフトウェア開発には最も適していると考えられていますが，現在のオブジェクト指向方法論はその形式性の低いことが原因で，発展的ソフトウェア開発に必要な意味内容に立ち入った計算機支援を行なうことが困難です． 我々のグループでは，オブジェクト指向方法論を形式的基盤のうえに展開し，構成されたソフトウェアの発展を可能にする原理やメカニズムについて研究を行ってきました． その結果，形式的な分析モデル記述体系，定理証明技術を中心とした分析モデル構築支援システム，分析モデル実行システムなどについて本質的な研究成果が得られ，オブジェクト指向方法論の上流工程を科学的ベースにのせることに，原理的には成功しました． さらに，組み込みシステムを対象にして，設計・実装工程の形式的扱いの研究を進めています．
ソフトウェアは一回作ればそれで良いとういうものでなく，利用環境や仕様の変化などに対応して，進化・発展させなければなりません． また，大規模なソフトウェアはその全容を捉えることが困難で，発展的にしか構成することができません． 現在，ソフトウェア発展のための技術は不十分で，発展のためのコストは非常に大きなものになっています． 我々のグループでは，代数的束や構成的数学にもとづくソフトウェア発展のための数学的理論や，抽象解釈にもとづく発展的構成法などの独自の研究成果をあげることが出来ました．
本シンポジウムでは，オブジェクト指向方法論の形式的展開に関する２つのデモを行ないます． 一つは，高階論理定理証明系HOLを中心にした分析モデル構築支援システムに関するのものです． もう一つは，分析モデル実行システムに関するものです．
本プロジェクトでは，コンピュータプログラムの自動超高速化システムWSDFU（Waseda Simplify-Distribute-Fold-Unfold，ウスドゥフ）の開発に成功した． それは，実測値として最高1億倍以上の自動高速化を達成している． しかも，多くの場合，自動高速化はパソコンを用いても瞬時（1分以内）に行える． 人が走る速さと光の速さとの差が3千万倍以下であることを思えば，1億倍の差異の大きさが実感できよう． このような桁違いの高速化を自動的に行うソフトウェアの開発は世界初である． WSDFUはまだ実験システムであるので，現段階では，高速化可能なプログラムの種類に制限がある． しかし，この成功により今後5年以内で制限を取除ける見通しが得られている． WSDFUが実用化された場合，次のようなことが期待できる：
その他にも，プログラムの性能および信頼性を評価するためのテストデータ―の自動生成ソフトウェア，プログラムの計算時間を自動評価するソフトウェア等を開発し，WWW上で公開した． また，線分や区間に関する問題解決をするプログラムの系統的作成法を発見した．
プログラム自動超高速化システムWSDFUを用いて，現実的プログラムを一瞬のうちに高速化するデモを行う． また，分割統治法を用いたプログラムの計算時間の評価を自動的に行うソフトウェアの使い方および有効性などを説明する．
米澤グループでは，未来開拓学術研究推進事業として，移動オブジェクトのためのプログラミング言語システムの理論・実装技術などの研究を行なってきました． ここで移動オブジェクトとは，ネットワーク上のコンピュータ間を自律的に移動できるプログラムのことです． そして，この研究の成果として現在までに，言語システムを構成する幾つかのソフトウェアを開発・公開してきました．
一方，（株）日本総合研究所事業化研究グループでは，来る大容量ネットワーク時代を睨み，次世代ネットワークソフトウェア配信システムの開発に取り組み始めました． そのシステムでは，単にソフトウェアをダウンロードするのとは違い，ソフトウェアのインストール，バージョンアップ，レンタル，配信に伴う料金自動徴収，なども機能として想定しています．
そして今回，その配信システムの開発の基礎技術として，米澤グループの移動オブジェクト技術を採用しました． 「移動するソフトウェア」という考え方が次世代のソフトウェア配信に適していると判断したからです． 今後，米澤グループ成果の一つであるJavaGOシステムを使って，次世代ネットワークソフトウェア配信システムの開発を進めて行く予定です．
本展示では，同社事業化研究グループと米澤グループが共同で実装を行なった，ソフトウェア配信システムのプロトタイプによる，自動インストールのデモを行ないます． このデモでは，会社や学校などのLANで，LAN内の各PCの利用者が希望するソフトウェアや，LANの保守上必要なソフトウェア（例えばワクチンソフト）を各PCにインストールするという場面を想定しています． このとき，各PC利用者がパソコン初心者だとしたら，例えばシステム管理者を雇うなりして，各PCへのインストール作業をしてもらうことになるでしょう． しかし，何十台，何百台というPCが相手では，時間やコストの面で非常に負担となります．
自動インストールシステムでは，移動オブジェクトが各PCへ自在に移動し，ソフトウェアの配信・インストール作業を行なってくれます． 管理者は管理サーバを操作・管理するだけで済みます． 展示では，実際にPC数台により構成されたLANを用意し，LANに接続された全てのPCに，自動的にソフトウェアのインストールを行う様子を見ることができます． さらに，このシステムは，悪意ある第三者による，ソフトウェアの盗難や，PCへのウィルス感染などの危険に対処するため，移動オブジェクト（含ソフトウェア）に対する暗号化や，電子捺印の付加なども行なうよう設計されています．
米崎グループでは，人間とのインタラクションを主体とするいわゆるリアクティブシステムの誤りの無い実現を得るために，仕様記述の段階からの科学的な方法に基づく開発方法，特に論理に基づく形式手法の背景で必要となる理論と，その実現について研究を行ってきました．
ソフトウェアはますます社会基盤として使われる場面が大きくなり，その誤りのない実現は，社会の安全性にとって非常に重要な問題となっております． また小さな製品でもそれが私たちの生活の中で大量に使われるものについては，そこに含まれる欠陥が，それを製造する企業の存続に影響する事態さえ，十分に想定されます．
このようなシステムは，リアクティブシステムとして捉えられる場合が多く，その実現の誤りを防ぐために，システムの仕様記述の段階で，実現可能であるか，危険な場合の見落としが無いかなどを予め検証して実現段階に進む方法を取ることは，その仕様記述や検証にかかるコストに十分見合うようになってきました．
我々のグループでは，このようなシステムの誤りの無い開発を，仕様記述レベルからサポートする方法の背景にある理論と，その理論に基づいたソフトウェア開発サポートシステムの実現方法について，時間論理を基礎として研究を行いました．
その結果，計算時間の膨大さから非現実的であると言われている仕様検証を現実のものとするための，独創的なアイデアに基づく原理的な方法を明らかにすると共に，いくつかの技術的ブレークスルーを行いました． この成果は，検証システムの基本となるタブロー証明エンジンの細かなチューンアップにも反映され，仕様検証器としては，これまでにない性能レベルを達成致しました．
本展示では，PLTLによって記述されたリアクティブシステムの仕様検証システムのデモを行います． 具体的には，充足可能性，段階的充足可能性，強充足可能性の各判定を行ないます． また，タブロー展開にBDDを改善して用いることによる効果についても説明を行います． さらにモジュールに分割された仕様の検証の効率化のための様々な手法，特に部分評価を用いる方法についても実演を行います．