時間制約付き制御フローグラフの弱双模倣等価性検証およびWebセキュリティ検査への応用(VLSIの設計/検証/テスト及び一般テスト)
スポンサーリンク
概要
- 論文の詳細を見る
近年、実時間制約を伴うハードウェア・ソフトウェアプログラムの効率的な開発手法が求められている。プログラム開発においては、プロファイラを用いた分岐構造の変更などが行われるが、そのような場合においても、入出力など外部観測点の間に指定された実時間制約が保存されていることを検証したい。そのような検証には、Global Timed Bisimulationの検証が有用である。本論文では、実時間制約が与えられたプロ,グラムから制御構造と時間制約を抽出したモデルである、Timed CFG (Control Flow Graph)のGlobal Timed Bisimulation等価性検証を、時間強双模倣等価性検証に帰着して行う手法を提案する。WebブラウザのTiming Attack に対する脆弱性検証への応用例も示す。
- 2003-11-27
著者
-
中田 明夫
広島市立大学大学院情報科学研究科
-
東野 輝夫
大阪大学大学院情報科学研究科
-
谷本 匡亮
大阪大学大学院情報科学研究科
-
中田 明夫
大阪大学大学院情報科学研究科
-
東野 輝夫
大阪大学大学院情報科学研究科|独立行政法人科学技術振興機構 Crest
-
佐々木 俊
大阪大学大学院情報科学研究科
-
東野 輝夫
大阪大学大学院情報学研究科
関連論文
- 災害現場でセンシングされた生体情報を集約する無線センサーネットワークの構成法(モバイルコンピューティング、モバイルアプリケーション、ユビキタス通信、モバイルマルチメディア通信)
- ネットワークオンチップにおける回路面積と配線コストを考慮したチップ内通信構造最適化の一手法(コンピュータシステムの設計・検証及び一般,デザインガイア2007-VLSI設計の新しい大地を考える研究会)
- 時間オートマトンのモデル検査(モデル検査,フォーマルアプローチ論文)
- アドホック通信に基づく行先経路の道路情報取得プロトコルの開発(セッション2,ITS情報処理・一般)
- アドホック通信に基づく行先経路の道路情報取得プロトコルの開発(セッション2)(ITS情報処理・一般)
- 詳細度の異なるモデルを用いた無線シミュレーションの高速化手法の提案(Work in Progress,ワイヤレス環境でのアプリケーション品質,P2P/アドホックネットワーク,画像符号化,ストリーム技術,信頼性,一般)
- 無線メッシュネットワークにおけるWDSクラスタ分割アルゴリズムの改善(無線ネットワーク)
- 災害医療支援ネットワークのための軽傷者用負傷者端末(システム設計,物理設計及び一般)
- 位置情報に基づくTDMプロトコルの提案(セッション1)
- 車車間通信を利用した信号機制御手法の提案
- 車車間通信を用いた危険車両の検出手法の提案(車車間通信技術,次世代社会基盤をもたらす高度交通システムとモバイル通信システム)
- メッセージフェリーと車車間通信を併用した渋滞情報収集システムの情報伝播効率の改善(車車間通信技術,次世代社会基盤をもたらす高度交通システムとモバイル通信システム)
- データ付時間オートマトンの双模倣等価性の記号的検証法
- 時間オートマトンのモデル検査
- MANETを用いた災害時における被災者の位置情報収集・追跡システムの提案(交通における計測・一般(電気系3学会ITS合同研究会))
- MANETを用いた災害時における被災者の位置情報収集・追跡システムの提案(交通における計測, 一般(電気系3学会ITS合同研究会))
- 1J-4 センサーネットワークの設計開発を支援するシミュレーション融合型テストベットの検討(情報爆発時代における情報提示・センサネット・P2P,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 無線メッシュネットワークのアクセスポイント間通信での優先度順リンク動作方式(トラヒックエンジニアリング,一般,トラヒック,NW評価,性能,リソース管理・制御,トラヒックエンジニアリング,NW信頼性・レジリエンシ,一般)
- 先行経路上の道路情報取得用アドホック通信プロトコルの開発(ITS)
- 目的地選択の公平性と指定されたノード密度分布を実現する移動モデルの提案(学生特別セッション,移動通信ワークショップ)
- 時間オートマトンにとる実時間システムの形式的検証
- 実時間ソフトウェア再利用のためのパラメトリック実行時間解析の一手法
- チップ内ネットワークの性能要求検証および最適化のための一手法(ネットワーク,通信)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法(FPGAとその応用及び一般)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法
- 部品のコスト・性能を考慮したリアルタイム組込みシステムの一設計法(VLSI設計技術とCAD)
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- 実時間通信システムに対する高信頼ハードウェア合成手法の提案(VLSIの設計/検証/テスト及び一般論理合成及び高位合成)
- 実時間通信システムに対する高信頼ハードウェア合成手法の提案(VLSIの設計/検証/テスト及び一般 論理合成及び高位合成)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- 並行周期EFSM群でモデル化されたQoSルータの高信頼性設計の一手法
- 並行周期EFSMに対するパラメトリックモデル検査手法(LAシンポジウム(計算機科学基礎理論ワークショップ)論文小特集)
- 並行周期EFSMに対するパラメトリックモデル検査およびパラメタ条件簡約高速化の一手法
- 遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証
- 無線センサーネットワークを利用した電子トリアージシステムの実現(モバイル/放送融合アプリケーション,モバイルコンテンツ,モバイル映像配信,一般)
- 無線センサーネットワークを利用した電子トリアージシステムの実現(学生特別セッション,モバイル/放送融合アプリケーション,モバイルコンテンツ,モバイル映像配信,一般)
- 傷病者の自動監視を実現する電子トリアージシステム(モバイル P2P,ユビキタスネットワーク,アドホックネットワーク,センサネットワーク,一般)
- NGNを活用したセキュア通信提供サービスの提案
- ノード群の相対位置関係に基づく位置推定アルゴリズムの評価手法
- 移動無線端末の位置情報と通信情報を用いた災害現場地図の自動生成
- 断続的に移動する無線端末群の位置推定
- 災害時救急救命支援に向けた電子トリアージシステムの設計開発
- 遭遇端末の位置情報と地理情報を併用した高精度な位置推定手法の提案と評価(ユビキタスネットワーク,ITS,センサーネットワーク,アドホックネットワーク)
- BP-7-5 オーバレイ・エージェントプラットフォームPIAXとその展開(BP-7.プラットフォーム化へ向かうユビキタス・センサネットワーク,パネルセッション,ソサイエティ企画)
- Deformable Templateマッチング法による唇輪郭抽出法の改良と歯科医療応用を目的とした評価(画像処理,画像パターン認識)
- Deformable-Templateマッチング法による唇輪郭抽出法の改良としきい値自動調整アルゴリズムの提案
- 関数合成による唇輪郭抽出法の提案
- Deformable-Templateマッチング法による唇輪郭抽出法の改良と内眼角点を原点とする座標系表現法の提案
- 都市街路における排気ガス量の削減を目的とする車車間通信を想定したリアルタイム信号制御手法の提案
- 計算負荷分散を考慮した近隣端末の分散型移動予測手法の提案
- センサネットワークアプリケーションの実装支援APIの実装と評価
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 先行道路情報取得プロトコルRMDPの設計と評価(ITS)
- 行先道路情報取得プロトコルRMDPの評価と車々間・路車間通信混在環境への適応(セッション7)(テーマ:モバイルコンピューティング,ITS,放送コンピューティング)
- 行先道路情報取得プロトコルRMDPの評価と車々間・路車間通信混在環境への適応(セッション7)(テーマ:モバイルコンピューティング,ITS,放送コンピューティング)
- チップ内ネットワークの性能要求検証および最適化のための一手法(ネットワーク,通信)
- チップ内ネットワークの性能要求検証および最適化のための一手法(ネットワーク,通信)
- チップ内ネットワークの性能要求検証および最適化のための一手法(ネットワーク,通信)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法(FPGAとその応用及び一般)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法(FPGAとその応用及び一般)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法(FPGAとその応用及び一般)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法
- リソーススケジューリングを考慮したUML MARTE振る舞い仕様の性能検証
- リソーススケジューリングを考慮したUML MARTE振る舞い仕様の性能検証
- リソーススケジューリングを考慮したUML MARTE振る舞い仕様の性能検証
- リソーススケジューリングを考慮したUML MARTE振る舞い仕様の性能検証
- N-025 3×3分割表を用いたテスト項目関連構造の分析(教育・人文科学,一般論文)
- 時相論理式を満足する実時間プロトコル仕様のパラメータ条件導出
- 時相論理式を満足する実時間プロトコル仕様のパラメータ条件導出
- 時間制約付き制御フローグラフの弱双模倣等価性検証およびWebセキュリティ検査への応用(VLSIの設計/検証/テスト及び一般テスト)
- 時間制約付き制御フローグラフの弱双模倣等価性検証およびWebセキュリティ検査への応用(VLSIの設計/検証/テスト及び一般 テスト)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- パラメタ付き時間インターバルオートマトンに対するパラメトリック検証の高速化手法 (計算機科学基礎理論とその応用)
- シナリオを用いたタスク及びバス転送へのサイクル割り当ての一手法(VLSIの設計/検証/テスト及び一般(デザインガイア))
- シナリオを用いたタスク及びバス転送へのサイクル割り当ての一手法(VLSIの設計/検証/テスト及び一般(デザインガイア))
- シナリオを用いたタスク及びバス転送へのサイクル割り当ての一手法(VLSIの設計/検証/テスト及び一般(デザインガイア))
- シナリオを用いたタスク及びバス転送へのサイクル割り当ての一手法(VLSIの設計/検証/テスト及び一般(デザインガイア))
- 実時間制約検証に特化したCANバスモデルの提案とシミュレータの試作(アーキテクチャ)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会)
- 実時間制約検証に特化したCANバスモデルの提案とシミュレータの試作(アーキテクチャ)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 実時間制約検証に特化したCANバスモデルの提案とシミュレータの試作(アーキテクチャ)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 実時間制約検証に特化したCANバスモデルの提案とシミュレータの試作(アーキテクチャ)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 再構成オーバーヘッドを考慮した動的再構成可能プロセッサへの実時間タスク群分割実装アルゴリズムの提案(タスクスケジューリング,組込技術とネットワークに関するワークショップETNET2008)
- 再構成オーバーヘッドを考慮した動的再構成可能プロセッサへの実時間タスク群分割実装アルゴリズムの提案(タスクスケジューリング,組込技術とネットワークに関するワークショップETNET2008)
- 再構成オーバーヘッドを考慮した動的再構成可能プロセッサへの実時間タスク群分割実装アルゴリズムの提案(タスクスケジューリング,組込技術とネットワークに関するワークショップETNET2008)
- 再構成オーバーヘッドを考慮した動的再構成可能プロセッサへの実時間タスク群分割実装アルゴリズムの提案(タスクスケジューリング,組込技術とネットワークに関するワークショップETNET2008)
- 動的リコンフィギャラブルプロセッサへの時間制約付き機能モジュール群分割アルゴリズムの検討(DRP,FPGA)
- 動的リコンフィギャラブルプロセッサへの時間制約付き機能モジュール群分割アルゴリズムの検討(DRP,FPGA)
- 動的リコンフィギャラブルプロセッサへの時間制約付き機能モジュール群分割アルゴリズムの検討(DRP,FPGA,組込技術とネットワークに関するワークショップETNET2007)
- 動的リコンフィギャラブルプロセッサへの時間制約付き機能モジュール群分割アルゴリズムの検討(DRP,FPGA,組込技術とネットワークに関するワークショップETNET2007)
- 安全な多重帰属制御を実現するVPN分散管理プロトコルの提案(ネットワークプロトコル,シームレスコンピューティングとその応用技術)
- データ付時間オートマトンの双模倣等価性の記号的検証法
- あるクラスの時間オートマトンに対する適合性試験系列生成の一手法(マルチメディア通信と分散処理)
- シミュレーションによるバス通信構造の設計改善を容易化するバスシステム設計支援ツールの提案(設計技術と設計自動化)
- Java言語による階層バス調停ポリシーを持つバスシステムのモデリング及びシミュレーション(コデザイン及びアーキテクチャ)
- Java言語による階層バス調停ポリシーを持つバスシステムのモデリング及びシミュレーション(コデザイン及びアーキテクチャ)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- リアルタイム組込みシステムの動的再構成可能プロセッサへの一実装方法の提案(アプリケーションI, デザインガイア-VLSI設計の新しい大地を考える研究会-)
- マルチランデブに基づくグループ通信機能を提供する Java ミドルウェアの提案
- Java言語による階層バス調停ポリシーを持つバスシステムのモデリング及びシミュレーション(コデザイン及びアーキテクチャ)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- 文脈自由プロセスに対するプロトコル合成の一手法