講演抄録/キーワード |
講演名 |
2012-05-31 11:20
誤差を有するシステムのシミュレーション結果に対する統計的解析とそのハードウェアによる高速化 ○大島浩資・小野翔平・松本剛史・藤田昌宏(東大) VLD2012-10 |
抄録 |
(和) |
変数値に誤差を有するシステムの解析手法として,統計的モデル検査を利用することができる.統計的モデル検査においてはシミュレーションが繰り返し実行され,その結果に対してプロパティチェックを行うが,プロパティに含まれる変数の数や扱う時間の範囲が大きければ,検査にかかる時間は長くなる.本稿では,統計的モデル検
査の高速化を目的として,BLTL 式のプロパティチェッカをFPGA 上に実装する手法を提案する.FPGA 上に実装されたプロパティチェッカを利用し,津波シミュレーションプログラムを例題として統計的モデル検査を行ったところ,ソフトウェアのみによる実行と比較して実行時間が約30 倍短縮された. |
(英) |
Statistical model checking is a method to analyze systems where variables have some uncertainty. It can be used to check some desired properties are satisfied with some specified probability under such uncertainty. In statistical model checking, the system needs to be simulated and checked for properties, repeatedly. The property checking takes a long time if a property includes many variables and/or a long time range. In this paper, we propose a hardware implementation of BLTL property checkers to accelerate the property checking process. Through the experimental results on Tsunami simulation, we show that the total execution time of statistical model checking can be shorten 30 times compared to a software implementation, by implementing our proposed BLTL property checkers on FPGA. |
キーワード |
(和) |
統計的モデル検査 / 有界線形時相論理 / FPGA / シミュレーション / / / / |
(英) |
statistical model checking / bounded linear temporal logic / FPGA / simulation / / / / |
文献情報 |
信学技報, vol. 112, no. 71, VLD2012-10, pp. 55-60, 2012年5月. |
資料番号 |
VLD2012-10 |
発行日 |
2012-05-23 (VLD) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
VLD2012-10 |