| 講演名 | 1995/5/30 時相論理式をベースとする並行ソフトウェアの検証 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 並行ソフトウェアは,多くのプロセスが並行動作してタイミング制約が厳しく,動作が正しいタイミングで行われるかどうかが非常に重要である.本稿では,リアルタイム時相論理の表現力を向上させた拡張TCTL(Timed CTL)を提案して,効率的なモデルチェッキング手法を提案する.本手法の主要な特徴は以下のとおりである.(1)稠密時間モデル上のFreeze quantificationとbounded temporal operatorの融合により,簡潔で表現力の高いタイミング制約表現が可能となる.(2)モデルチェッキングは不等式手法とラベリング手法の融合により実現する. |
| 抄録(英) | Concurrent software consists of many concurrent processes and behaves on strict timing conditions. In this paper, I propose extended TCTL(Timed TCTL) and effective real-time model checking as follows. (1)The timing description of extended TCTL consists of both freeze quantification and bounded temporal operator. For this extension, extended TCTL admits timing constraints between distant contexts. (2)Real time model checking consists of both labelling algorithm and inequalities method. |
| キーワード(和) | 並行ソフトウェア / 仕様記述 / タイミング検証 / リアルタイムモデルチェッキング |
| キーワード(英) | concurrent software / specification / timing verification / real-time model checking |
| 資料番号 | |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 1995/5/30(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 時相論理式をベースとする並行ソフトウェアの検証 |
| サブタイトル（和） | |
| タイトル（英） | Verification of concurrent software based on real-time logic |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 並行ソフトウェア / concurrent software |
| キーワード(2)（和/英） | 仕様記述 / specification |
| キーワード(3)（和/英） | タイミング検証 / timing verification |
| キーワード(4)（和/英） | リアルタイムモデルチェッキング / real-time model checking |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 1 著者 所属（和/英） | 島根大学理学部情報科学科 Dept. of Computer science Faculty of Science Shimane University |
| 発表年月日 | 1995/5/30 |
| 資料番号 | |
| 巻番号（vol） | vol.95 |
| 号番号（no） | 86 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |