| 講演名 | 1994/11/17 時間∀-オートマトンによるリアルタイムシステムの設計手法 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 望ましいリアルタイムシステムの仕様記述の要件は状態と動作の概念や時相表現からの記述である.本稿では,∀-オートマトンに注目して,時間∀-オートマトンによる仕様記述と検証の手法を提案する.本手法の主要な特徴は以下の通りである:(1)稠密時間領域のタイミング制約記述の拡張により時間∀-オートマトンを考案する.(2)仕様記述と検証性質記述は統一的に状態と動作の概念や時相表現により,ダイヤグラム的に時間∀-オートマトンで行う.(3)検証方式はシステム仕様と検証性質仕様との言語包合問題である.事例を通して,本手法の有効性を示す. |
| 抄録(英) | It is necessary to specify real-time system from the standpoint of both states and behaviors,and temporal representation.In this paper,I propose timed ∀-atutomaton,which extends Manna's ∀-atutom aton by timing constraints specification and mechanical verification.My proposal method consists of specification by timed ∀-atutomaton,and language inclusion problem by real-time logic.Thi s method is shown effective by example. |
| キーワード(和) | リアルタイムシステム / 仕様記述 / 検証 / 時間∀-オートマトン / タイミング制約 |
| キーワード(英) | real-time system / specification / verification / timed ∀-atuto maton / timing constraints |
| 資料番号 | SS94-40 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1994/11/17(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 時間∀-オートマトンによるリアルタイムシステムの設計手法 |
| サブタイトル（和） | |
| タイトル（英） | Specification Method of real-time system using timed ∀-automaton |
| サブタイトル（和） | |
| キーワード(1)（和/英） | リアルタイムシステム / real-time system |
| キーワード(2)（和/英） | 仕様記述 / specification |
| キーワード(3)（和/英） | 検証 / verification |
| キーワード(4)（和/英） | 時間∀-オートマトン / timed ∀-atuto maton |
| キーワード(5)（和/英） | タイミング制約 / timing constraints |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 1 著者 所属（和/英） | 島根大学理学部情報科学科 Department of Computer Science,Faculty of Science,Shimane University |
| 発表年月日 | 1994/11/17 |
| 資料番号 | SS94-40 |
| 巻番号（vol） | vol.94 |
| 号番号（no） | 334 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |