確率時間CEGARの開発とその実証実験

• 清水, 隆也

• 森下, 篤

• 山根, 智

Bibliographic Information

Other Title

• カクリツ ジカン CEGAR ノ カイハツ ト ソノ ジッショウ ジッケン
• Development and Experiments of Probabilistic Timed CEGAR

Abstract

本論文では，確率時間オートマトンの到達可能性解析に述語抽象化と反例を用いた精錬の枠組み（CEGAR）を適用する手法を提案する．CEGARを用いることにより，組込システムのようなリアルタイム動作，確率動作を持つシステムに対する，効率的な自動検証が可能となる．

In this paper, we present an efficient verification method for probabilistic timed automaton. This method based on predicate abstraction and refinement realizes effective automated verifications for real-time and probabilistic embedded systems.

Journal

• 情報処理学会論文誌プログラミング（PRO）

  情報処理学会論文誌プログラミング（PRO） 5 (2), 43-66, 2012-03-30

  東京 : 情報処理学会

Keywords

• 通常論文

Details

• CRID: 1050282812878532992
• NII Article ID: 40019257054
• NII Book ID: AA11464814
• ISSN: 18827802
• ISSN: 18827772
• ISSN: 03875806
• NDL BIB ID: 023636907
• Web Site: http://id.nii.ac.jp/1001/00081615/
• Web Site: http://id.ndl.go.jp/bib/023636907
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I023636907
• Text Lang: ja
• Article Type: article
• Data Source:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN