2000 Fiscal Year Annual Research Report
| Project/Area Number |
12133206
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas (B)
|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
飯田 周作 日本学術振興会, 特別研究員
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
森 彰 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30311682)
|
|---|
| Keywords | 安全性検証 / 振舞仕様 / セキュアプロトコル / 実時間システム / 移動コード / 抽象機械 |
|---|
| Research Abstract |
実時間システム(real-time syste),セキュアプロトコル(secure protocol),抽象機械(abstract machine),移動コード(mobile code),等の,ネットワーク社会において重要な役割を担うソフトウェアシステムの安全性を,よりユーザーやアプリケーションに近いレベルで検証するための基盤として,以下のような研究を行った.
[並行,分散,実時間システムの検証]知られている並行・分散・実時間システムの代表的なモデルに基づき,CafeOBJの形式仕様が自然に作成でき,それらに基づき半自動的な検証も行えることが,非同期データ送受信,相互排除アルゴリズム,分散相互排除アルゴリズム,実時間システム,などに分類される幾つかの基本的な問題について確かめられた.
[Javaバイトコード検証器の形式仕様]Javaコードの安全性の解析すをめざし,Javaアプレットの安全性確保における中核をなすJavaバイトコード検証器の代数仕様言語CafeOBJによるJBJ仕様の開発を行った.基礎となるJava Bytecode Verifier(JBV)のCafeOBJ仕様の開発が終わっり,CafeOBJ処理系により記号実行を行ない,幾つかの性質を記号実験的に確かめることが出来ることを確かめた.
[モデル検査に基づく移動コードの安全性検証]移動コードの安全性検証に関して,本年度までに,移動コードの安全性を保証するための基礎技術として,代数仕様を用いたモデル検査についての研究を行った.具体的には,代数仕様言語システムCafeOBJ上で自動定理証明器PigNoseの開発を行い,これを用いた安全性モデル検査の実験を行った.実験では,証明携帯コードの例題も取り上げ,本研究における手法が移動コードの安全性保証において有用であるとの知見を得た.
|
-
[Publications] 飯田周作,二木厚吉: "振舞仕様に基づく仕様コンポーネント化技術の発展可能ソフトウェアへの応用"コンピュータソフトウェア別冊ソフトウェア発展. 30-45 (2001)
-
[Publications] Diaconescu,R.,Futatsugi,K.,Iida,S.: "CafeOBJ jewels"CAFE : An Industiral-Strength Algebraic Formal Method. 33-60 (2000)
-
[Publications] Goguen,J.,Lin,K.,Rosu,G,Mori,A.,Warinschi,B.: "An overview of Tatami project"CAFE : An Industiral-Strength Algebraic Formal Method. 61-78 (2000)
-
[Publications] Goguen,J.,Winkler,T.,Meseguer,J.,Futatsugi,K.: "Introducing OBJ"Software Engineering with OBJ. 3-167 (2000)
-
[Publications] Seino,T.,Ogata,K.,Futatsugi,K.: "Specification and verification of a single-track railroad signaling in CafeOBJ"Proc.of 2000 Int'l Technical Conference on Circuits/Systems, Computers and Communications(ITC-CSCC 2000). 268-273 (2000)
-
[Publications] Nakamura,M.,Ogata,K.: "The evaluation strategy for head normal form with and without on-demand flags"Electronic Notes in Theoretical Computer Science (Proc.of the 3rd Int'l Workshop on Rewriting Logic and its Applications). 36. (2001)
