| 講演名 | 2000/5/11 リアルタイムソフトウェアの形式化と検証 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | リアルタイムソフトウェアは外部環境と相互作用があり, タイミング制約が厳しく, 並行プロセスにより構成される.このため仕様が正しいことを保証することが重要である.本論文では, 時間ステートチャートを用いて, 並行性やタイミング制約, 機能の統合的な仕様記述を行う.さらに, Pnueliらのクロック遷移システムにより, 時間ステートチャートの意味を定義する.それを基にして, 演繹的証明により, 時間ステートチャートが安全性や活性を充足することが検証できることを示す.最後に, 時間ステートチャートを抽象化して, 時間オートマトンのシンボリック検証器KRONOSを使い, 自動演繹的検証できることを示す.そして, 演繹的検証と自動演繹的検証を実験的に評価して, 定量的に, 自動演繹的検証が優れていることを示す. |
| 抄録(英) | Hard real-time software 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 timed statechart. Moreover, we represent semantics of timed statechart using Pnueli's clocked transition systems. Next, we verify whether timed statechart satisfy safety and liveness properties or not by deductive proofs. Finally, we transform timed statechart into timed automaton by abstract techniques and automatically verify timed automaton by KRONOS. We show automated deductive verification is better than deductive verification by empirical studies. |
| キーワード(和) | リアルタイムソフトウェア / 時間ステートチャート / 演繹的検証 / 自動演繹的検証 |
| キーワード(英) | real-time software / timed statechart / automated deduction / deductive verification |
| 資料番号 | SS2000-5 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2000/5/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | リアルタイムソフトウェアの形式化と検証 |
| サブタイトル（和） | |
| タイトル（英） | Formalization and Verification for Real-Time Software |
| サブタイトル（和） | |
| キーワード(1)（和/英） | リアルタイムソフトウェア / real-time software |
| キーワード(2)（和/英） | 時間ステートチャート / timed statechart |
| キーワード(3)（和/英） | 演繹的検証 / automated deduction |
| キーワード(4)（和/英） | 自動演繹的検証 / deductive verification |
| 第 1 著者 氏名（和/英） | 山根 智 / SATOSHI YAMANE |
| 第 1 著者 所属（和/英） | 鹿児島大学工学部情報工学科 Dept.of Information and Computer Science, Kagoshima University |
| 発表年月日 | 2000/5/11 |
| 資料番号 | SS2000-5 |
| 巻番号（vol） | vol.100 |
| 号番号（no） | 63 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |