離散確率分布を持つリアルタイムシステムの詳細化検証手法

• 山根, 智

Bibliographic Information

Other Title

• リサン カクリツ ブンプ オ モツ リアルタイム システム ノ ショウサイカ ケンショウ シュホウ
• Formal Refinement Verification Method of Real time Systems with Discrete Probability Distributions
• 検証/テストとデバッグ

Abstract

近年，リアルタイムシステムの仕様記述言語としては，タイミング制約が記述可能な時間オートマトンが定着しており，その検証手法としてもモデル検査手法などが開発されている．一方，最近，不確かな動作を表現するために，離散確率分布を持つ確率時間オートマトンが開発されており，そのモデル検査手法も開発されている．本論文では，離散確率分布を持つ確率時間オートマトンの時間模倣関係の検証手法を開発して，リアルタイムシステムの段階的詳細化開発への適用を図る．

Generally, real-time systems have been specified using timed automata,and moreover model-checking methods of timed automata have been developed.On the other hand, recently,probabilistic timed automata have been developed in order to expressthe relative likelihood of the system exhibiting certain behavior.In this paper,we develope the verification method of simulation relation of probabilistic timed automata,and apply this method into stepwise refinement developments of real-time systems.

Journal

• 情報処理学会論文誌

  情報処理学会論文誌 44 (8), 2189-2199, 2003-08-15

  東京 : 電子情報通信学会

Keywords

• 論文

Details

• CRID: 1050564287837260032
• NII Article ID: 110002711814
• NII Article ID: 110003276634
• NII Book ID: AN00116647
• ISSN: 18827764
• ISSN: 09135685
• ISSN: 03875806
• NDL BIB ID: 6467571
• NDL BIB ID: 6679259
• Web Site: http://id.nii.ac.jp/1001/00011171/
• Web Site: http://id.ndl.go.jp/bib/6467571
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I6467571
• Web Site: http://id.ndl.go.jp/bib/6679259
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I6679259
• Text Lang: ja
• Article Type: journal article
• Data Source:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN