WEKO3
インデックスリンク
アイテム
離散確率分布を持つリアルタイムシステムの詳細化検証手法 (検証 / テストとデバッグ)
http://hdl.handle.net/2297/23625
http://hdl.handle.net/2297/2362500270902-653c-4c31-b107-fa2bf7445f0a
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
TE-PR-YAMANE-S-2189.pdf (905.8 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2017-10-03 | |||||
| タイトル | ||||||
| タイトル | 離散確率分布を持つリアルタイムシステムの詳細化検証手法 (検証 / テストとデバッグ) | |||||
| タイトル | ||||||
| タイトル | Formal Refinement Verification Method of Real-time Systems with Discrete Probability Distributions (Verification, Testing, and Debugging) | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | journal article | |||||
| 著者 |
山根, 智
× 山根, 智 |
|||||
| 提供者所属 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 金沢大学理工研究域電子情報学系 | |||||
| 書誌情報 |
Transactions of Information Processing Society of Japan = 情報処理学会論文誌 巻 44, 号 8, p. 2189-2199, 発行日 2003-08-15 |
|||||
| ISSN | ||||||
| 収録物識別子タイプ | ISSN | |||||
| 収録物識別子 | 0387-5806 | |||||
| NCID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AN00116647 | |||||
| 出版者 | ||||||
| 出版者 | Information Processing Society of Japan (IPSJ) = 情報処理学会 | |||||
| 抄録 | ||||||
| 内容記述タイプ | 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 express the 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. | |||||
| 権利 | ||||||
| 権利情報 | 本文データは情報処理学会の許諾に基づきCiNiiから複製したものである | |||||
| 著者版フラグ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://www.ipsj.or.jp/ | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://ci.nii.ac.jp/naid/110002711814/en/ | |||||
