時間ペトリネットでモデル化された非同期システムに対するモデル検査ツールUPPAALの適用
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,非同期システムの一種である GALS(大域非同期局所同期)システムの特性を,モデル検査ツール UPPAAL を用いて検証する手法を提案する.ここでは,STPN(確率時間ペトリネット) でモデル化された GALS システムを対象として,与えられた STPN を UPPAAL の入力形式である XTA(拡張時間オートマトン) へと変換することで,UPPAAL による検証を行う.提案法では,STPN の各プレイスの振る舞いを XTA で表現し,同期チャネルを用いて XTA 間を同期することで STPN 全体の振る舞いを表現する.最後に,例題へと提案法を適用してその有効性を示すとともに,従来手法との比較も合わせて行う.
- 2011-07-14
著者
-
近藤 真史
岡山県立大学大学院情報系工学研究科
-
佐藤 洋一郎
静大農
-
佐藤 洋一郎
岡山県立大学情報工学部情報システム工学科
-
横川 智教
岡山県立大学情報工学部情報システム工学科
-
宮崎 仁
岡山県立大学大学院情報系工学研究科システム工学専攻
-
佐藤 洋一郎
人間文化研機構地球研
-
横川 智教
岡山県立大学情報工学部
-
佐藤 洋一郎
岡山県立大学 情報工学部 情報システム工学科
関連論文
- D-7-12 動画像による健常者の膝関節運動機能解析法の検討(D-7. MEとバイオサイバネティックス,一般セッション)
- 回胴式遊技機(パチスロ)から放射される中間周波磁界及び高周波電界に関する基礎的検討(電磁環境・EMC)
- Stochastic Timed Petri Net でモデル化した大規模論理回路の性能評価ツール
- リングセグメント型Globally Asynchronous Locally Synchronous Systemの構成法(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- モデル検査ツールUPPAALを用いたGALSシステムの形式的検証(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- インドシナにおける稲遺伝資源の収集 -17年間のまとめ-
- イネ遺伝資源の特性評価と利用4.ミャンマー由来の野生イネ
- 記号モデル検査を用いた状態マシン図とシーケンス図の無矛盾性の検証(設計支援)
- 有界モデル検査を用いた複数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領域の塩基配列によるサクラ属サクラ亜属の遺伝的特徴づけ
- サクラ亜属におけるPS-ID領域の多型
- Globally Asynchronous Locally Synchronous Systemの性能評価に関する一検討(上流設計技術(2),システムオンシリコン設計技術並びにこれを活用したVLSI)
- 射影変換の高速化に関する一検討(演算回路/専用回路,システムオンシリコン設計技術並びにこれを活用したVLSI)
- 日本産ヒエ属にみられるマイクロサテライトおよびISSR領域における多型
- RAPD法による日本列島のクスノキ巨樹の遺伝的多様性
- 中国・城頭山遺跡から出土したイネ種子のwaxy座の解析
- 登呂遺跡から出土したイネ籾殻の形態的遺伝的変異
- 出土炭化米のDNA分析からにたイネと稲作の起源
- 日中韓の水稲品種のマイクロサテライト多型
- ウズベキスタン共和国,ダルヴェルジン・テペから出土した植物遺体
- DNA多型によるウルシの系統分化
- DNAマーカによる栽培ヒエと野生ヒエの判別
- 射影変換における座標計算の高速化手法(画像・映像処理)
- D-11-139 射影変換における座標計算の高速化手法 : 誤差の評価(D-11.画像工学D)
- パーソナルユースを指向した動画像用幾何学変換器の実現法
- パーソナルユースを指向した動画像用幾何学変換器の実現法
- 記号モデル検査を用いたシステムの耐故障性の自動検証手法の提案
- ソフトウェア開発プロジェクトのリアルタイム管理を目的とした支援システム(ソフトウェア開発環境・開発支援システム, システム開発論文)
- 描画時合成方式と表示時合成方式の併用によるスムーズ操作が可能なマルチウィンドウシステム(計算機システム)
- 地球環境問題と育種の貢献 : 第114回秋季シンポジウム「東南アジアにおけるイネ育種の現場と地球環境変動下における今後のイネ育種課題」によせて
- ブータン国にみられたイネ細胞質多型の地理的勾配
- SQUIDの二つのしきい値を利用した超伝導論理回路の構成法(計算機構成要素)
- CMOS D フリップフロップのカスケード接続により構成したシンクロナイザの性能評価式
- CMOSにより構成したシンクロナイザの性能評価式
- CMOSにより構成したシンクロナイザの性能評価式
- CMOSにより構成したシンクロナイザの性能評価式
- シンクロナイザの一性能評価法
- PS-ID領域の塩基配列に基づくクリ属4種の分類
- 競合処理用ジョセフソンフリップフロップの一構成法
- 同一構造の二つの機能ブロックを用いた長方形動画像用アフィン変換器
- 同一構造の二つの機能ブロックを用いた長方形動画像用アフィン変換器
- 同一構造の二つの機能ブロックを用いた長方形動画像用アフィン変換器
- CMOS Dフリップフロップにおけるメタステーブル動作の組織的軽減法
- 長方形動画像のための1アフィン変換法
- 機能モジュールを用いた動画像用アフィン変換器
- 本誌〔食の科学〕11月号掲載「食品化学余話"クリは栽培されていたか?"」に答える 食の安全とフードシステムの改革
- 考古学とDNA分析 (特集 21世紀の日本考古学) -- (日本考古学の新しいうねり)
- 無題
- SSR多型に基づく古代イネの分類
- 第2集 北の縄文・南の縄文 (縄文農耕を捉え直す)
- 人類はどんな穀物酒を飲んできたか(バイオミディア2003)
- 人類はどんな穀物酒を飲んできたか
- DNAマーカを用いたカシの分類(IV)3つの葉緑体DNA領域によるブナ科植物の識別および近縁関係
- マイクロサテライトによるカシ(Quercus)の分類
- 時間ペトリネットでモデル化された非同期システムに対するモデル検査ツールUPPAALの適用
- LTSAを用いたシーケンス図の詳細化関係の検証
- B-4-10 複数の回胴式遊技機による放射中間周波磁界の遊技者への影響評価(B-4. 環境電磁工学,一般セッション)
- タブーサーチを用いた臨床実習スケジューリングの自動化
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法 (回路とシステム)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法 (システム数理と応用)
- AS-1-2 GALSシステムを対象としたペトリネットシミュレーションにおけるアービタのモデル化(AS-1.モデリングとシミュレーションの最新動向,シンポジウムセッション)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法(グラフ,ペトリネット,ニューラルネット,及び一般)
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法(グラフ,ペトリネット,ニューラルネット,及び一般)
- 日本のイネの育種過程における遺伝的多様性の推移
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法
- ペトリネットシミュレーションの高速化を指向した接続行列の一生成法
- GPGPUを用いた透視化マルチウィンドウの一高速合成手法(視覚とIMQ一般)
- Globally Asynchronous Locally Synchronous Systemにおける非同期バスの一構成法(計算機システム)
- B-027 時間ペトリネットでモデル化されたGALSシステムを対象としたUPPAALによる自動検証手法(ソフトウェアサイエンス,B分野:ソフトウェア)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- C-016 多様な資源を対象とした多資源非同期式アービタの一構成(システム設計,C分野:ハードウェア・アーキテクチャ)
- メタステーブル動作持続時間を隠蔽するツリー型非同期式アービタ(システムと信号処理及び一般)
- 状態マシン図を用いたスマートフォンアプリのモデル化
- 状態マシン図を用いたスマートフォンアプリのモデル化