| 講演名 | 1999/3/19 ハードリアルタイムシステムの実時間記号モデル検査 館 宜伸, 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 以下のような特徴を持つ実時間記号モデル検査を開発した. 1. 実時間記号モデル検査のシステムは二分決定グラフによりシンポリンクに表現する. この手法において, 時間オートマトンから時間Kripke構造に変換して検証をおこなう. 2. 実時間システムにおいて, 近似解法を用いることにより検証コストを削減することができる. 3. 近似解法における実時間時相論理式のforwardとbackwardの不動点計算を行う. |
| 抄録(英) | We develop real time symbolic model checking that have following points. 1. The system of real time symbolic model checking expresses by BDDs. In this method, it verify to replace from timed automaton to timed Kripke structure. 2. In real time system, it can reduce verification costs by computing approximations. 3. In computing appoximations, it compute fixpoint of TCTL by both forward and backward. |
| キーワード(和) | 実時間システム / 時間オートマトン / 実時間記号モデル検査 / 実時間時相論理 |
| キーワード(英) | real time systems timed automaton / real time symbolic model checking / TCTL |
| 資料番号 | SS98-68 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1999/3/19(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | ハードリアルタイムシステムの実時間記号モデル検査 |
| サブタイトル（和） | |
| タイトル（英） | Real-time Symbolic Model Checking for Hard real-time system |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 実時間システム / real time systems timed automaton |
| キーワード(2)（和/英） | 時間オートマトン / real time symbolic model checking |
| キーワード(3)（和/英） | 実時間記号モデル検査 / TCTL |
| キーワード(4)（和/英） | 実時間時相論理 |
| 第 1 著者 氏名（和/英） | 館 宜伸 / Y. Tachi |
| 第 1 著者 所属（和/英） | 島根大学理学部情報科学科計算機科学講座 Dept. of Computer and Information Science, Shimane University |
| 第 2 著者 氏名（和/英） | 山根 智 / S. Yamane |
| 第 2 著者 所属（和/英） | 島根大学理学部情報科学科計算機科学講座 Dept. of Computer and Information Science, Shimane University |
| 発表年月日 | 1999/3/19 |
| 資料番号 | SS98-68 |
| 巻番号（vol） | vol.98 |
| 号番号（no） | 676 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |