| 研究概要 |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.並行プログラムのための統一的型システムの考案
前年度までに特定の性質を保証するための型システムを数種類構築することに成功したが,現実には保証したい性質はシステムごとに異なり,保証する性質ごとに検証システムを構築するのは非現実的である.そこで,さまざまな性質を統一的に検証するための型システムを考案した.この型システムに基づいて検証システムを構築すれば,一部を変更するだけで,さまざまな性質を検証することが可能になる.
2.ライブロックフリーダムを保証する型システムの考案
並行プログラムにおいて,特定の通信がいずれ必ず成功することを保証する型システムを構築した.さらにその発展として,一定時間内に通信が必ず成功することを保証する型システムも構築した.
3.考案済みの型システムの現実のプログラミング言語への応用
前年度までに考案した個々の性質を保証するための型システムの現実のプログラムに対する有効性を検証し,必要であれば上記統一的型システムに改良を加えるために,現実のプログラミング言語に適用する試みを開始した.具体的には(1)並行プログラミング言語CMLのためのデッドロックフリーダムの検証器の構築,(2)Java言語のバイトコード中でのオブジェクトのロックの獲得・解放の整合性を検査するシステムの構築を開始した.
|
