WEKO3
アイテム
動的再構成システムの仕様化と検証
https://ipsj.ixsq.nii.ac.jp/records/21725
https://ipsj.ixsq.nii.ac.jp/records/217251f46a687-ead3-4ec2-ae48-adac0a553cc0
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SE97117004.pdf (751.8 kB)
|
Copyright (c) 1997 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1997-11-21 | |||||||
| タイトル | ||||||||
| タイトル | 動的再構成システムの仕様化と検証 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Specification and Validation of a Dynamically Reconfigurable System | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 仙台電波工業高等専門学校 | ||||||||
| 著者所属 | ||||||||
| 仙台電波工業高等専門学校 | ||||||||
| 著者所属 | ||||||||
| 仙台電波工業高等専門学校 | ||||||||
| 著者所属 | ||||||||
| 仙台電波工業高等専門学校 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Sendai National College of Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Sendai National College of Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Sendai National College of Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Sendai National College of Technology | ||||||||
| 著者名 |
板橋, 吾一
加納稔久
高橋, 薫
加藤, 靖
× 板橋, 吾一 加納稔久 高橋, 薫 加藤, 靖
|
|||||||
| 著者名(英) |
Goichi, Itabashi
Toshihisa, Kano
Kaoru, Takahashi
Yasushi, Kato
× Goichi, Itabashi Toshihisa, Kano Kaoru, Takahashi Yasushi, Kato
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 分散並行システムにおいては，リンクを経由してシステム構成要素間で通信が行われ，所望の分散アプリケーションが達成される．リンクが静的ではなく動的に構成・確立されるのであれば，システムは動的再構成システムとして複雑化を呈することになる．本稿では，システム構成要素を有限状態機械の概念でモデル化し，それらが動的にリンクを確立・解消しながら並行実行するような動的再構成システム仕様の挙動検証を可能とする方法について検討し，検証システムの実装を行う． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | In a distributed concurrent system such as a computer communication net-work, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal speciflcation of such a dynamically reconfigurable system in, which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and released. We also present an algorithm to validate the safety and link-related properties in the specifled behavior. Finally, we design and implement a validator that enables validation of the given specification. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN10112981 | |||||||
| 書誌情報 |
情報処理学会研究報告ソフトウェア工学（SE） 巻 1997, 号 110(1997-SE-117), p. 25-32, 発行日 1997-11-21 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
