| 講演名 | 2015-11-20 分散アルゴリズムの実行列からプログラム合成とそのプログラム検証 山根 智(金沢大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 分散システムの分散問題を解決する分散アルゴリズムはクラウドコンピュータやP2Pなどで多数動作しており, その正当性検証は重要な研究である．本論文では, メッセージパッシング型の非同期分散システムを対象として, 時空ダイアグラムで表現されるような分散アルゴリズムの事象列から, プロセス代数流の操作的意味論により, プログラムを合成する手法を提案する. さらに, 時相論理の演繹的証明により, 合成したプログラムの正当性を検証する手法を提案する. 以上により, 分散アルゴリズムの正当性を検証する. |
| 抄録(英) | Distributed algorithms are executed on distributed systems such as cloud computing and P2P. It is important to verify distributed algorithms. Here we focus on popular distributed systems with asynchronous message passing. In this paper, we propose program synthesis method from event sequences of distributed algorithm represented by space-time diagrams based on operational semantics of process algebra. Also, we verify synthesized program by temporal proof method. By the above mentioned method, we verify distributed algorithms. |
| キーワード(和) | 分散アルゴリズム / プログラム合成 / プログラム検証 / プロセス代数 / 時相論理 / 操舵的意味 |
| キーワード(英) | distributed algorithm / program synthesis / program verification / process algebra / temporal logic / operational semantics |
| 資料番号 | CAS2015-50,MSS2015-24 |
| 発行日 | 2015-11-13 (CAS, MSS) |
| 研究会情報 | |
| 研究会 | MSS / CAS / IPSJ-AL |
|---|---|
| 開催期間 | 2015/11/20(から2日開催) |
| 開催地（和） | 指宿市民会館 大会議室 |
| 開催地（英） | Ibusuki CityHall |
| テーマ（和） | グラフ、ペトリネット、ニューラルネット及び一般 |
| テーマ（英） | |
| 委員長氏名（和） | 山根 智(金沢大) / 田中 聡(村田製作所) |
| 委員長氏名（英） | Satoshi Yamane(Kanazawa Univ.) / Satoshi Tanaka(Murata) |
| 副委員長氏名（和） | 名嘉村 盛和(琉球大) / 高橋 俊彦(新潟大) |
| 副委員長氏名（英） | Morikazu Nakamura(Univ. of Ryukyus) / Toshihiko Takahashi(Niigata Univ.) |
| 幹事氏名（和） | 中田 充(山口大) / 豊嶋 伊知郎(東芝) / 山脇 大造(日立) / 越田 俊介(東北大) |
| 幹事氏名（英） | Mitsuru Nakata(Yamaguchi Univ.) / Ichiro Toyoshima(Toshiba) / Taizou Yamawaki(Hitachi) / Shunsuke Koshita(Tohoku Univ.) |
| 幹事補佐氏名（和） | 金城 秀樹(沖縄大) / 橘 俊宏(湘南工科大) / 中村 洋平(日立) |
| 幹事補佐氏名（英） | Hideki Kinjo(Okinawa Univ.) / Toshihiro Tachibana(Shonan Inst. of Tech.) / Yohei Nakamura(Hitachi) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Mathematical Systems Science and its applications / Technical Committee on Circuits and Systems / Special Interest Group on Algorithms |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 分散アルゴリズムの実行列からプログラム合成とそのプログラム検証 |
| サブタイトル（和） | |
| タイトル（英） | Program syntesis from execution traces andt its program verification of distributed algorithms |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 分散アルゴリズム / distributed algorithm |
| キーワード(2)（和/英） | プログラム合成 / program synthesis |
| キーワード(3)（和/英） | プログラム検証 / program verification |
| キーワード(4)（和/英） | プロセス代数 / process algebra |
| キーワード(5)（和/英） | 時相論理 / temporal logic |
| キーワード(6)（和/英） | 操舵的意味 / operational semantics |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 1 著者 所属（和/英） | 金沢大学(略称：金沢大) Kanazawa University(略称：Kanazawa Univ.) |
| 発表年月日 | 2015-11-20 |
| 資料番号 | CAS2015-50,MSS2015-24 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | CAS-315,MSS-316 |
| ページ範囲 | pp.35-40(CAS), pp.35-40(MSS), |
| ページ数 | 6 |
| 発行日 | 2015-11-13 (CAS, MSS) |