時間ペトリネットでモデル化された非同期システムに対するモデル検査ツールUPPAALの適用

• Item type: SIG Technical Reports(1)
• 公開日: 2011-07-14
• タイトル: 時間ペトリネットでモデル化された非同期システムに対するモデル検査ツールUPPAALの適用
• タイトル / 言語: en
• タイトル: Verifying Asynchronous Systems Modeled by Timed Petri Nets Using UPPAAL
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 形式手法
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者名: 三輪, 陽介; 横川, 智教; 宮崎, 仁; 近藤, 真史; 佐藤, 洋一郎
• 著者名(英): Yosuke, Miwa; Tomoyuki, Yokogawa; Hisashi, Miyazaki; Masafumi, Kondo; Yoichiro, Sato
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，非同期システムの一種である GALS(大域非同期局所同期)システムの特性を，モデル検査ツール UPPAAL を用いて検証する手法を提案する．ここでは，STPN(確率時間ペトリネット) でモデル化された GALS システムを対象として，与えられた STPN を UPPAAL の入力形式である XTA(拡張時間オートマトン) へと変換することで，UPPAAL による検証を行う．提案法では，STPN の各プレイスの振る舞いを XTA で表現し，同期チャネルを用いて XTA 間を同期することで STPN 全体の振る舞いを表現する．最後に，例題へと提案法を適用してその有効性を示すとともに，従来手法との比較も合わせて行う．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we propose a method to verify a GALS system modeled by an STPN(Stochastic Timed Petri Net) using model checker UPPAAL. For this purpose, we propose the method to convert STPN to XTA(eXtended Timed Automata), which is an input of UPPAAL. In our method, the places in the STPN are represented by an XTA, and they are synchronized by using broadcast channels. We also develop a tool to convert a file describing the structure of a STPN to XTA as an input format of UPPAAL. Finally, we carried out a comparison experiment of the size of generated model and the cost of verification by UPPAAL.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2011-SE-173, 号 2, p. 1-7, 発行日 2011-07-14
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会