モデル検査ツールUPPAALを用いたGALSシステムの形式的検証(ネットワークオンチップ,システムオンシリコンを支える設計技術)
スポンサーリンク
概要
- 論文の詳細を見る
GALS(Globally Asynchronous Locally Synchronous)システムの設計では,設計したシステムが意図した通りに動作することを検証する必要がある.GALSシステムは非同期通信を行うため,検証を行うには連続時間性を考慮してモデル化しなければならない.しかし,従来の検証手法ではこの点が十分に考慮されていなかった.本研究では,連続時間に基づく検証ツールUPPAALを用いて,GALSシステムの設計を形式的に検証する手法を提案している.STPN(Stochastic Timed Petri Nets)でモデル化されたGALSシステムを,UPPAALで扱う拡張時間オートマトンに変換する手法を提案し,ツールとして実装している.適用例として,STPNで記述されたGALSシステムに提案法を適用して検証を行い,手法の有効性を確認している.
- 2009-03-04
著者
-
佐藤 洋一郎
岡山県立大学情報工学部情報システム工学科
-
横川 智教
岡山県立大学情報工学部情報システム工学科
-
宮崎 仁
岡山県立大学大学院情報系工学研究科
-
佐藤 洋一郎
岡山県立大学情報工学部
-
早瀬 道芳
岡山県立大学
-
桐田 和明
岡山県立大学
-
宮崎 仁
岡山県立大学大学院情報系工学研究科システム工学専攻
-
早瀬 道芳
岡山県立大学大学院情報系工学研究科
-
横川 智教
岡山県立大学情報工学部
-
横川 智教
岡山県立大学大学院情報系工学研究科
-
佐藤 洋一郎
岡山県立大学 情報工学部 情報システム工学科
-
横川 智教
岡山県立大学 情報工学部 情報システム工学科
関連論文
- D-7-12 動画像による健常者の膝関節運動機能解析法の検討(D-7. MEとバイオサイバネティックス,一般セッション)
- 回胴式遊技機(パチスロ)から放射される中間周波磁界及び高周波電界に関する基礎的検討(電磁環境・EMC)
- Stochastic Timed Petri Net でモデル化した大規模論理回路の性能評価ツール
- リングセグメント型Globally Asynchronous Locally Synchronous Systemの構成法(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- モデル検査ツールUPPAALを用いたGALSシステムの形式的検証(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- 記号モデル検査を用いた状態マシン図とシーケンス図の無矛盾性の検証(設計支援)
- 有界モデル検査を用いた複数UML図の形式的検証
- D-3-3 有界モデル検査を用いた複数UML図の検証に関する検討(D-3.ソフトウェアサイエンス,一般講演)
- Globally Asynchronous Locally Synchronous Systemの性能評価に関する一検討(上流設計技術(2),システムオンシリコン設計技術並びにこれを活用したVLSI)
- 射影変換の高速化に関する一検討(演算回路/専用回路,システムオンシリコン設計技術並びにこれを活用したVLSI)
- K_067 透視化機能をもつマルチウィンドウシステムの高解像度化(K分野:ヒューマンコミュニケーション&インタラクション)
- B_003 シーケンス図と状態遷移図で記述されたUMLモデルを対象としたモデル検査による形式的検証(B分野:ソフトウェア)
- D-11-97 漸化式表現による再構成型幾何学変換器(D-11.画像工学D(画像処理・計測),一般講演)
- D-11-64 多眼カメラによるモザイク動画像生成に関する研究(D-11.画像工学D(画像処理・計測),一般講演)
- D-10-1 モデル検査手法を用いたUML図の検証(D-10.ディペンダブルコンピューティング,一般講演)
- C-024 ウィンドウの透視化と輝度低下機能を持つマルチウィンドウシステムの評価(C分野:アーキテクチャ・ハードウェア)
- D-11-69 射影変換を対象としたDRAM-SRAM間画像転送法(D-11. 画像工学B(画像デバイス・装置), 情報・システム2)
- D-11-27 RISC命令の並列実行機能を有する画像処理用DSP(D-11. 画像工学A(画像基礎・符号化), 情報・システム2)
- C-019 操作対象ウィンドウの透視化機能を持つマルチウィンドウシステム(C.アーキテクチャ・ハードウェア)
- A-4-27 大規模ディジタルシステムのSTPNによるモデル化(A-4. ディジタル信号処理)
- D-10-14 メタステーブル動作を考慮したリングアービタのペトリネット表現
- 半構造データにおけるスキーマ抽出問題の計算複雑さ
- D-6-6 高速マルチウィンドウシステムのハードウエアアーキテクチャ
- オブジェクト指向データベースにおける逆行を含む属性集合とその閉包を用いた経路式を経由するクラスの一探索法
- グラフデータベースにおける正規表現及び文脈自由文法を満たす最短経路の一探索法
- D-6-17 高速マルチウィンドウ合成方式における画像データの格納方法
- ラオス北部のイネ・モチ遺伝子の多型
- ラオス中部のモチイネ品種におけるSSR多型
- SSRマーカーに基づく九州産ヤマザクラの遺伝的多様性について
- サクラ属における葉緑体DNAの解析 : 1. 葉緑体3領域における変異
- イネ在来系統'赤毛'から生じた新規変異体の遺伝解析
- 葉緑体rpl16-rpl14領域の塩基配列によるサクラ属サクラ亜属の遺伝的特徴づけ
- Globally Asynchronous Locally Synchronous Systemの性能評価に関する一検討(上流設計技術(2),システムオンシリコン設計技術並びにこれを活用したVLSI)
- 射影変換の高速化に関する一検討(演算回路/専用回路,システムオンシリコン設計技術並びにこれを活用したVLSI)
- 日本産ヒエ属にみられるマイクロサテライトおよびISSR領域における多型
- 射影変換における座標計算の高速化手法(画像・映像処理)
- D-11-139 射影変換における座標計算の高速化手法 : 誤差の評価(D-11.画像工学D)
- パーソナルユースを指向した動画像用幾何学変換器の実現法
- パーソナルユースを指向した動画像用幾何学変換器の実現法
- 記号モデル検査を用いたシステムの耐故障性の自動検証手法の提案
- ソフトウェア開発プロジェクトのリアルタイム管理を目的とした支援システム(ソフトウェア開発環境・開発支援システム, システム開発論文)
- 描画時合成方式と表示時合成方式の併用によるスムーズ操作が可能なマルチウィンドウシステム(計算機システム)
- 描画時合成方式と表示時合成方式とを併用したマルチウィンドウ合成方式
- 地球環境問題と育種の貢献 : 第114回秋季シンポジウム「東南アジアにおけるイネ育種の現場と地球環境変動下における今後のイネ育種課題」によせて
- SQUIDの二つのしきい値を利用した超伝導論理回路の構成法(計算機構成要素)
- 非長方形ウィンドウの高速操作機能を備えたマルチウィンドウシステムの実現法
- DRAMセルアレーを用いた動画像用アフィン変換器の一構成法
- ウィンドウの重なりを制御するデータセレクタの一構成法
- CMOS D フリップフロップのカスケード接続により構成したシンクロナイザの性能評価式
- CMOSにより構成したシンクロナイザの性能評価式
- CMOSにより構成したシンクロナイザの性能評価式
- CMOSにより構成したシンクロナイザの性能評価式
- シンクロナイザの一性能評価法
- シンクロナイザの性能評価
- λ-幾何における3点の最小スタミナ木のスタイナ点位置
- 競合処理用ジョセフソンフリップフロップの一構成法
- 同一構造の二つの機能ブロックを用いた長方形動画像用アフィン変換器
- 同一構造の二つの機能ブロックを用いた長方形動画像用アフィン変換器
- 同一構造の二つの機能ブロックを用いた長方形動画像用アフィン変換器
- CMOS Dフリップフロップにおけるメタステーブル動作の組織的軽減法
- 長方形動画像のための1アフィン変換法
- 機能モジュールを用いた動画像用アフィン変換器
- 帰還を用いたメタステーブル動作持続期間の短縮法
- 本誌〔食の科学〕11月号掲載「食品化学余話"クリは栽培されていたか?"」に答える 食の安全とフードシステムの改革
- 考古学とDNA分析 (特集 21世紀の日本考古学) -- (日本考古学の新しいうねり)
- 無題
- 第2集 北の縄文・南の縄文 (縄文農耕を捉え直す)
- 人類はどんな穀物酒を飲んできたか(バイオミディア2003)
- 人類はどんな穀物酒を飲んできたか
- 命令実行により検査するときのプロセッサ制御回路のテスト生成問題
- 時間ペトリネットでモデル化された非同期システムに対するモデル検査ツールUPPAALの適用
- LTSAを用いたシーケンス図の詳細化関係の検証
- メタステ-ブル動作にもとづくリングア-ビタ誤動作の分散
- デジ-チェン・ア-ビタのメタステ-ブル動作にもとづくMTBF
- 高速ウィンドウ操作を指向したマルチウィンドウ合成方式
- 順序回路の代数的仕様とその検証 : モジュール数がパラメータ化されている場合
- メタステーブル動作を模擬するための CMOS NOR ゲートモデル
- 要求先取り形ア-ビタのMTBF
- リングア-ビタのメタステ-ブル動作にもとづくMTBF
- メタステ-ブル動作を模擬するためのRSフリップフロップモデル(技術談話室)
- 純遅延を考慮したRSフリップフロップのメタステ-ブル動作解析
- タブーサーチを用いた臨床実習スケジューリングの自動化
- AS-1-2 GALSシステムを対象としたペトリネットシミュレーションにおけるアービタのモデル化(AS-1.モデリングとシミュレーションの最新動向,シンポジウムセッション)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法(グラフ,ペトリネット,ニューラルネット,及び一般)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法(グラフ,ペトリネット,ニューラルネット,及び一般)
- 日本のイネの育種過程における遺伝的多様性の推移
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法
- GPGPUを用いた透視化マルチウィンドウの一高速合成手法(視覚とIMQ一般)
- Globally Asynchronous Locally Synchronous Systemにおける非同期バスの一構成法(計算機システム)
- B-027 時間ペトリネットでモデル化されたGALSシステムを対象としたUPPAALによる自動検証手法(ソフトウェアサイエンス,B分野:ソフトウェア)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- C-016 多様な資源を対象とした多資源非同期式アービタの一構成(システム設計,C分野:ハードウェア・アーキテクチャ)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- 状態マシン図を用いたスマートフォンアプリのモデル化
- 状態マシン図を用いたスマートフォンアプリのモデル化
- エネルギー保存を考慮した画素値分布推定法(画像処理・符号化及び一般)