| 研究概要 |
実時間システム(real-time syste),セキュアプロトコル(secure protocol),抽象機械(abstract machine),移動コード(mobile code),等の,ネットワーク社会において重要な役割を担うソフトウェアシステムの安全性を,よりユーザーやアプリケーションに近いレベルで検証するための基盤として,以下のような研究を行った.
[並行,分散,実時間システムの検証]知られている並行・分散・実時間システムの代表的なモデルに基づき,CafeOBJの形式仕様が自然に作成でき,それらに基づき半自動的な検証も行えることが,非同期データ送受信,相互排除アルゴリズム,分散相互排除アルゴリズム,実時間システム,などに分類される幾つかの基本的な問題について確かめられた.
[Javaバイトコード検証器の形式仕様]Javaコードの安全性の解析すをめざし,Javaアプレットの安全性確保における中核をなすJavaバイトコード検証器の代数仕様言語CafeOBJによるJBJ仕様の開発を行った.基礎となるJava Bytecode Verifier(JBV)のCafeOBJ仕様の開発が終わっり,CafeOBJ処理系により記号実行を行ない,幾つかの性質を記号実験的に確かめることが出来ることを確かめた.
[モデル検査に基づく移動コードの安全性検証]移動コードの安全性検証に関して,本年度までに,移動コードの安全性を保証するための基礎技術として,代数仕様を用いたモデル検査についての研究を行った.具体的には,代数仕様言語システムCafeOBJ上で自動定理証明器PigNoseの開発を行い,これを用いた安全性モデル検査の実験を行った.実験では,証明携帯コードの例題も取り上げ,本研究における手法が移動コードの安全性保証において有用であるとの知見を得た.
|
