| 講演名 | 2006-11-10 モデル検査によるステートチャートとシーケンスチャートの整合性検証(「さまざまな分野の形式的検証最前線」及びAI一般) 長谷川 哲夫, 深澤 良彰, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 多種のシステムを低コストで短期間に開発しなければならない組込みソフトウェアなどの分野でもモデル検査手法のような設計検証技術が容易に使えるようになることに期待が高まっている.時間制約のあるシステムでは,動的な挙動をシーケンスチャートで定義し,ステートチャートでプロセスの静的な挙動を定義することが多い.性能モデル検査はプロセス毎のステートチャートと同等の時間オートマトンで定義された挙動を検証するものであるが検証したい性質を時相論理式で与える点が,設計者にとって利用の敷居を高くしている理由の1つである.本稿では,モデル検査ツールUPPAALを対象として,シーケンスチャートから検証したい性質を表現するオブザーバを機械的に生成する手法を提案し,通信プロトコルのアプリケーションに適用してオーバーヘッドの評価を行った. |
| 抄録(英) | In the software field of embedded systems, where many kinds of systems must be developed in a short term and low-cost, a model checking that is one of automatic design verification techniques is expected to be easy to use for a software designers. In this paper, a method generating an observer for the model checking tool UPPAAL from sequence charts, which is usually made by designers, is proposed. Also it is reported the result of applying this method to a communication system. |
| キーワード(和) | モデル検査 / 設計検証 / リアルタイムシステム / UML / ステートチャート / シーケンスチャート |
| キーワード(英) | model checking / real time system / UML / state chart / sequence chart |
| 資料番号 | AI2006-19 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2006/11/3(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モデル検査によるステートチャートとシーケンスチャートの整合性検証(「さまざまな分野の形式的検証最前線」及びAI一般) |
| サブタイトル（和） | |
| タイトル（英） | Consistency analysis between state charts and sequence charts by model checking |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / model checking |
| キーワード(2)（和/英） | 設計検証 / real time system |
| キーワード(3)（和/英） | リアルタイムシステム / UML |
| キーワード(4)（和/英） | UML / state chart |
| キーワード(5)（和/英） | ステートチャート / sequence chart |
| キーワード(6)（和/英） | シーケンスチャート |
| 第 1 著者 氏名（和/英） | 長谷川 哲夫 / Tetsuo HASEGAWA |
| 第 1 著者 所属（和/英） | 早稲田大学:株式会社 東芝 Waseda University:Toshiba corporation |
| 第 2 著者 氏名（和/英） | 深澤 良彰 / Yoshiaki FUKAZAWA |
| 第 2 著者 所属（和/英） | 早稲田大学 Waseda University |
| 発表年月日 | 2006-11-10 |
| 資料番号 | AI2006-19 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 340 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |