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