講演抄録/キーワード |
講演名 |
2009-06-03 16:50
[招待講演]確率時間CEGAR ○森下 篤・駒形龍太・山根 智(金沢大) CST2009-5 |
抄録 |
(和) |
本論文では, 確率時間オートマトンの到達可能性解析に述語抽象化とその精錬の枠組み(CEGAR)を適用する手法を提案する. CEGAR を用いることにより, 組込システムのようなリアルタイム動作, 確率動作を持つシステムに対する, 効率的な自動検証が可能となる. |
(英) |
In this paper, we present an efficient verification method for probabilic timed automaton. This method based on predicate abstraction and refinement enables effective automated verification for real-time and probabilistic embedded systems. |
キーワード |
(和) |
形式的検証 / 確率時間オートマトン / 到達可能性解析 / 述語抽象化 / 反例による精錬 / / / |
(英) |
Formal Method / Probabilistic Timed Automaton / Reachability Analysis / Predicate Abstraction / Counter Example Guided Refinement / / / |
文献情報 |
信学技報, vol. 109, 2009年6月. |
資料番号 |
|
発行日 |
2009-05-27 (CST) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
CST2009-5 |