| 講演名 | 2001/1/15 代数仕様言語CafeOBJによる実時間システムの仕様記述と検証の一例 : timed two-process raceの仕様記述と検証 清野 貴博, 緒方 和博, 二木 厚吉, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 元々, リアクティブシステムのモデル化を念頭に作られた形式手法であっても, 記述上の工夫によって実時間システムのモデル化に使うことができる.本稿では, N.Lynchが提案したGeneral Timed Automaton(GTA)を元に, 代数仕様言語であるCafeOBJの振舞仕様を使って実時間システムを扱う方法を考察する.この一事例としてtimed two-process raceと名付けた簡単な例題について, GTAを元にしたスタイルを用いて仕様記述を行い, その仕様がある安全性を持つことについて, invariant assertionの手法を用いて形式的検証を行う. |
| 抄録(英) | Formal methods that have been designed to model reactive systems can be used to model real-time systems. In this paper, we propose a way to specify real-time systems in CafeOBJ an algebraic specification language based on General Timed Automaton (GTA) model proposed by N. Lynch. As a case study, we formally specify a simple example called 'timed two-process race' in CafeOBJ based on GTA model, and verify that this system has a safety property based on the specification with invariant assertions with the help of the CafeOBJ system. |
| キーワード(和) | 形式手法 / CafeOBJ / 実時間システム |
| キーワード(英) | Formal methods / CafeOBJ / Real-time systems |
| 資料番号 | SS2000-32 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2001/1/15(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 代数仕様言語CafeOBJによる実時間システムの仕様記述と検証の一例 : timed two-process raceの仕様記述と検証 |
| サブタイトル（和） | |
| タイトル（英） | An example of specification and verification of real-time systems with CafeOBJ : timed two-process race |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式手法 / Formal methods |
| キーワード(2)（和/英） | CafeOBJ / CafeOBJ |
| キーワード(3)（和/英） | 実時間システム / Real-time systems |
| 第 1 著者 氏名（和/英） | 清野 貴博 / Takahiro Seino |
| 第 1 著者 所属（和/英） | 北陸先端科学技術大学院大学 情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology |
| 第 2 著者 氏名（和/英） | 緒方 和博 / Kazuhiro Ogata |
| 第 2 著者 所属（和/英） | 北陸先端科学技術大学院大学 情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology |
| 第 3 著者 氏名（和/英） | 二木 厚吉 / Kokichi Futatsugi |
| 第 3 著者 所属（和/英） | 北陸先端科学技術大学院大学 情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology |
| 発表年月日 | 2001/1/15 |
| 資料番号 | SS2000-32 |
| 巻番号（vol） | vol.100 |
| 号番号（no） | 569 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |