ログイン 新規登録
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

  1. 研究報告
  2. ソフトウェア工学(SE)
  3. 2013
  4. 2013-SE-181

調停者の選出方法を考慮した分散合意アルゴリズムのPROMELAモデルと検証

https://ipsj.ixsq.nii.ac.jp/records/94188
https://ipsj.ixsq.nii.ac.jp/records/94188
f575f682-c225-43d9-b2df-7870e3f1d43d
名前 / ファイル ライセンス アクション
IPSJ-SE13181008.pdf IPSJ-SE13181008.pdf (326.2 kB)
Copyright (c) 2013 by the Information Processing Society of Japan
オープンアクセス
Item type SIG Technical Reports(1)
公開日 2013-07-10
タイトル
タイトル 調停者の選出方法を考慮した分散合意アルゴリズムのPROMELAモデルと検証
言語
言語 jpn
キーワード
主題Scheme Other
主題 モデル
資源タイプ
資源タイプ識別子 http://purl.org/coar/resource_type/c_18gh
資源タイプ technical report
著者所属
信州大学大学院理工学系研究科情報工学専攻
著者所属
信州大学工学部情報工学科
著者名 後藤亮馬 和崎克己

× 後藤亮馬 和崎克己

後藤亮馬
和崎克己

Search repository
論文抄録
内容記述タイプ Other
内容記述 合意問題は分散システムの研究分野において重要な問題の一つであり,非同期分散アルゴリズムにおいては,合意問題が解決されているかを確認することが困難である.本研究では,非同期分散アルゴリズムの正当性を,モデル検査によって検証することを目的として,モデル検査器 SPIN を用いて,非同期分散合意アルゴリズムである Chandra-Toueg アルゴリズムの正当性を検証する.SPIN とは通信プロトコルの検証を目的として提案されたモデル検査ツールであり,使用記述言語 PROMELA で記述された振る舞いを,網羅探査により検査することができる.モデルの作成を行う際には,PROMELA 本来の記述方法では困難であった表現を行うために,グローバルタイムアウト機構などのいくつかの工夫を行った.Chandra-Toueg アルゴリズムで使用されている巡回調停者方式では,調停者が健全か否かを考慮しない.また,実際には調停者変更を行った後,ノード間でのリセット動作などの同期を取るべきである.以上二つの理由から,調停者変更時に健全性の判定機能を追加し,調停者変更後に同期をとる選出方法に変更した.作成した通常モデルと拡張モデルを使用してデットロック検査を行い,正当性を検証した.
書誌レコードID
収録物識別子タイプ NCID
収録物識別子 AN10112981
書誌情報 研究報告ソフトウェア工学(SE)

巻 2013-SE-181, 号 8, p. 1-7, 発行日 2013-07-10
Notice
SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
出版者
言語 ja
出版者 情報処理学会
戻る
0
views
See details
Views

Versions

Ver.1 2025-01-21 14:43:51.685439
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3