| 講演名 | 2003/1/23 離散確率分布を持つリアルタイムシステムの詳細化検証手法 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 近年,リアルタイムシステムの仕様記述言語としては,タイミング制約が記述可能な時間オートマトンが定着しており,その検証手法としてもモデル検査手法などが開発されている.一方,最近,不確かな動作を表現するために,離散確率分布を持つ確率時間オートマトンが開発されており,そのモデル検査手法も開発されている.本論文では,離散確率分布を持つ確率時間オートマトンの時間模倣関係の検証手法を開発して,リアルタイムシステムの段階的詳細化開発への適用を図る. |
| 抄録(英) | 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. |
| キーワード(和) | リアルタイムシステム / 確率時間オートマトン / 確率時間模倣関係 |
| キーワード(英) | real-time systems / probabilistic timed automata / probabikistic timed simulation relations |
| 資料番号 | SS2002-31 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2003/1/23(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 離散確率分布を持つリアルタイムシステムの詳細化検証手法 |
| サブタイトル（和） | |
| タイトル（英） | Formal Refinement Varification Method of Real-Time Systems with Discrete Probability Distributions |
| サブタイトル（和） | |
| キーワード(1)（和/英） | リアルタイムシステム / real-time systems |
| キーワード(2)（和/英） | 確率時間オートマトン / probabilistic timed automata |
| キーワード(3)（和/英） | 確率時間模倣関係 / probabikistic timed simulation relations |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi YAMANE |
| 第 1 著者 所属（和/英） | 金沢大学工学部情報システム工学科 Faculty of Engineering, Kanazawa University |
| 発表年月日 | 2003/1/23 |
| 資料番号 | SS2002-31 |
| 巻番号（vol） | vol.102 |
| 号番号（no） | 616 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |