| 講演名 | 1994/9/3 無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法 山根 智, 梅原 伸年, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | タイミング制約記述を含む非同期型並行システムの仕様は時間グラフで表現されることが多い.並行システムの計算機化のアプローチとしては,仕様の制約式からモデル生成する自動生成アプローチと,仕様が性質記述を充足するかどうかを判定する検証アプローチに分類できる.時間厳密性を含む時相論理式から稠密的時間領域な時間グラフを生成するモデル生成アルゴリズムは知られていないが,検証は決定可能である.そこで,我々は,時間グラフを効率的に仕様記述して検証するために,無限列時間付きステートチャートを考案した.その主要な特徴は,(1)時間オートマトンを拡張したステートチャートにより形式的に仕様記述する,(2)ステートチャートの検証問題を形式言語理論の言語包合問題に帰着する,(3)時間グラフのタイミングシミュレーションにより検証コストを削減する,(4)インターフェースルールにより検証性質毎に時間グラフを縮少する,である. |
| 抄録(英) | Asynchronus concurrent system specification which includes timing constraints,is usually expressed by timed graph.The approach of computer support for the concurrent system is classified into automatic generation(model generation from constraint temporal logic specification)and automatic vetification(deciding whether or not timed graph satisfies property).It is difficult to generate dense timed graph from temporal logic including punctuality.But automatic verification approach is decidable.We propose infinite timed statechart in order to effectively specify concurrent system and verify it.The main feature is following:(1)Formal specification by statechart extending timed automata.(2)Verification problem reduces to inclusion problem in formal language theory.(3)Timing simulation of timed graph largely reduces verification complexity.(4) Interface rule reduces space complexity of timed graph according to each verification property specification. |
| キーワード(和) | 並行システム / 仕様記述 / 検証 / ステートチャート / タイミング制約 / 時間オートマト ン |
| キーワード(英) | concurrent system / specification / verification / statechart / timing constraint / timed automaton |
| 資料番号 | CAS94-55 |
| 発行日 |
| 研究会情報 | |
| 研究会 | CAS |
|---|---|
| 開催期間 | 1994/9/3(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Circuits and Systems (CAS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 無限列時間付きステートチャートによる並行システムの仕様記述と検証の手法 |
| サブタイトル（和） | |
| タイトル（英） | Method of Specification and Verification of Concurrent System using infinite timed statechart |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 並行システム / concurrent system |
| キーワード(2)（和/英） | 仕様記述 / specification |
| キーワード(3)（和/英） | 検証 / verification |
| キーワード(4)（和/英） | ステートチャート / statechart |
| キーワード(5)（和/英） | タイミング制約 / timing constraint |
| キーワード(6)（和/英） | 時間オートマト ン / timed automaton |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 1 著者 所属（和/英） | 島根大学理学部情報科学科 Department of Computer and Information Science,Faculty of Science, Shimane University |
| 第 2 著者 氏名（和/英） | 梅原 伸年 / Nobutoshi Umehara |
| 第 2 著者 所属（和/英） | 島根大学理学部情報科学科 Department of Computer and Information Science,Faculty of Science, Shimane University |
| 発表年月日 | 1994/9/3 |
| 資料番号 | CAS94-55 |
| 巻番号（vol） | vol.94 |
| 号番号（no） | 214 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |