| 講演名 | 2000/1/18 時間ステートチャートによる仕様記述と演繹的検証 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | ハードリアルタイムシステムは外部環境との相互作用があり, タイミング制約が厳しく, 並行プロセスにより構成される.このために, 仕様が正しいことを保証することが重要である.本論文では, 時間ステートチャートを提案して, 並行性やタイミング制約, 機能の統合的な仕様記述を実現する.さらに, Pnueliらのクロック遷移システムにより, 時間ステートチャートの操作的意味を表現する.それを基にして, 演繹的証明により, 時間ステートチャートが安全性や活性を充足することが検証できることを示す.最後に, クロック遷移システム上で詳細化検証の公理系を開発して, 時間ステートチャートの詳細化の検証を示す. |
| 抄録(英) | Hard real-time systems have ongoing interactions with external environments, and consist of concurrent processes. It is important to verify whether hard real-time systems satisfy safety and liveness properties or not. In this paper, we integrally specify concurrency and timing constraints, functions using our proposed timed statechart. Moreover, we represent operational semantics of timedstatechart using Pnueli's clocked transition systems. Next we can verify whether timed statechart satisfy safety and liveness properties or not by deductive proofs. Finally, we propose a refinement verification rule and verify whether concretespecification refines abstract specification or not. |
| キーワード(和) | 時間ステートチャート / 演繹的検証 / 時相論理 / 詳細化検証 |
| キーワード(英) | timed statechart / deductive verification / temporal logic / refinement |
| 資料番号 | SS99-54 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2000/1/18(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 時間ステートチャートによる仕様記述と演繹的検証 |
| サブタイトル（和） | |
| タイトル（英） | Fomal specification and deductive verification based on Timed Statechart |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 時間ステートチャート / timed statechart |
| キーワード(2)（和/英） | 演繹的検証 / deductive verification |
| キーワード(3)（和/英） | 時相論理 / temporal logic |
| キーワード(4)（和/英） | 詳細化検証 / refinement |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 1 著者 所属（和/英） | 鹿児島大学工学部情報工学科 Dept. of computer science, Kagoshima university |
| 発表年月日 | 2000/1/18 |
| 資料番号 | SS99-54 |
| 巻番号（vol） | vol.99 |
| 号番号（no） | 547 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |