| 講演名 | 2001/1/15 論理関数を用いた並行システムにおけるデッドロック検出手法の提案と評価 徳田 勇祐, 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本論文では論理関数を用いた並行システムにおけるデッドロック検出手法の提案とその評価を行なう.並行システムは複数の有限オートマトンでモデル化されるものと仮定する.一般に並行システムの自動検証では, 状態爆発の問題をどう扱うかが重要となる.この問題はシステムにおいて多くのプロセスが相互作用する場合に生じ, システムの自動検証が非常に困難となる.この問題に対処する代表的な方法として論理関数を用いる手法と遷移の可換性を利用して状態を削減する半順序法とが知られている.デッドロック検出問題に対してこれらの方法の比較評価を行なった研究として文献[5]が良く知られている.しかしながら, この研究で用いられている論理関数に基づく方法には誤りがあり, 実際にはデッドロックの検出は不可能である.そこで, 本研究では両手法の再評価を試みる.まず論理関数を用いたデッドロック検出手法を新たに提案する.提案法では遷移関数を表す論理関数の操作によってデッドロック状態を始めに求め, その後に可到達解析を行なう.この提案法を実装し, 多くの並行システムの例に対する適用実験を通じて, 半順序法との比較評価を行なった.この結果に基づいて各手法がどのような並行システムに対して有効であるかを考察する. |
| 抄録(英) | In this paper, we propose a boolean function-based deadlock detection method for concurrent systems that are modeled as a set of communicating finite automata. The major problem with automated analysis of concurrent systems is dealing with state explosion problem. This problem occurs in systems with many processes that can interact with each other. Boolean function-based techniques and partial order reduction techniques are the two most common approaches to this problem. In a previous paper [5], these two approaches are compared with respect to performance in deadlock detection. However, the boolean function-based method used in this paper is flawed ; thus the results are not reliable. In this paper, we re-perform the comparison by developing a new boolean function-based deadlock detection method, In the method, the set of deadlock states is computed by manipulating the transition relation function, and then reachability analysis is used for deadlock detection. We implement this detection method and apply it to a variety of examples to perform comparative evaluation of these two methods. |
| キーワード(和) | 論理関数 / 並行システム / デッドロック検出 / BDD / 記号表現 |
| キーワード(英) | boolean function / concurrent system / deadlock detection / BDD / symbolic representation |
| 資料番号 | SS2000-34 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2001/1/15(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 論理関数を用いた並行システムにおけるデッドロック検出手法の提案と評価 |
| サブタイトル（和） | |
| タイトル（英） | Design and Evaluation of a Boolean Function-Based Deadlock Detection Method for Concurrent Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 論理関数 / boolean function |
| キーワード(2)（和/英） | 並行システム / concurrent system |
| キーワード(3)（和/英） | デッドロック検出 / deadlock detection |
| キーワード(4)（和/英） | BDD / BDD |
| キーワード(5)（和/英） | 記号表現 / symbolic representation |
| 第 1 著者 氏名（和/英） | 徳田 勇祐 / Yusuke Tokuda |
| 第 1 著者 所属（和/英） | 大阪大学 大学院基礎工学研究科 情報数理系専攻 Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro Tsuchiya |
| 第 2 著者 所属（和/英） | 大阪大学 大学院基礎工学研究科 情報数理系専攻 Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 第 3 著者 氏名（和/英） | 菊野 亨 / Tohru Kikuno |
| 第 3 著者 所属（和/英） | 大阪大学 大学院基礎工学研究科 情報数理系専攻 Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 発表年月日 | 2001/1/15 |
| 資料番号 | SS2000-34 |
| 巻番号（vol） | vol.100 |
| 号番号（no） | 569 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |