確率線形ハイブリッドオートマトンの到達可能性検証

• 畠中, 克也

• 山根, 智

Bibliographic Information

Other Title

• カクリツ センケイ ハイブリッドオートマトン ノ トウタツ カノウセイ ケンショウ
• Reachability Verification of Probabilistic Linear Hybrid Automata

Abstract

リアルタイムシステムに対するモデル検査の需要は増加しており，時間オートマトンで記述したモデルを検証可能なUPPAALに代表される検証器の開発がさかんに行われている．本研究では，コスト付き確率時間オートマトンのモデル検査のprocedureを拡張し，確率線形ハイブリッドオートマトンに対する検証を可能にする．さらに，モデルに対する検証を自動化するため，拡張したprocedureを計算機上に実装する．ケーススタディとして，無線センサネットワークをとりあげ，確率線形ハイブリッドオートマトンによるモデル化と，その検証例を示す．

Model checking is a formal method exhaustively verifying whether behaviors of a system satisfy specific characteristics. It can be applied to specification, testing or debugging stages. Priced probabilistic timed automata (PPTAs) can be used to model real-time systems with probability and cost features. In this paper, We define probabilistic linear hybrid automata (PLHAs), which are superclass of PPTAs. PLHA has real-valued variables proportional to time and discrete probabilistic distributions. Furthermore, we extend an procedure for cost-bounded probabilistic reachability problem in PPTAs. The procedure performs operations on convex polyhedra which presents symbolic states in PLHAs. As a case study, the paper presents simplified model of wireless sensor networks by use of parallel composition of PLHAs. PPTA can't handle this model because the model has multiple costs. Our verification program enables automatic verification for the such model.

Journal

• 情報処理学会論文誌

  情報処理学会論文誌 53 (12), 2671-2681, 2012-12-15

  東京 : 情報処理学会

Keywords

• [特集：組込みシステム工学] 確率線形ハイブリッドオートマトン，モデル検査，到達可能性解析，Fourier-Motzkin消去法，無線センサネットワーク

Details

• CRID: 1050564287855446272
• NII Article ID: 110009493416
• NII Book ID: AN00116647
• ISSN: 18827764
• ISSN: 18827837
• ISSN: 03875806
• NDL BIB ID: 024167776
• Web Site: http://id.nii.ac.jp/1001/00087738/
• Web Site: http://id.ndl.go.jp/bib/024167776
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I024167776
• Text Lang: ja
• Article Type: journal article
• Data Source:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN