文献

J-GLOBAL ID：202202257713133679   整理番号：22A0691450

分散動的再構成プロトコルの形式的検証【JST・京大機械翻訳】

Formal verification of a distributed dynamic reconfiguration protocol

著者 (3件)： Schultz William (Northeastern University, USA) ,  Dardik Ian (Northeastern University, USA) ,  Tripakis Stavros (Northeastern University, USA)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2022  ページ： 143-152  発行年： 2022年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： MongoRaftRe構成,分散動的再構成プロトコルの形式,機械チェックTLA+安全性証明を提示した。MongoRaftRe構成は,Raftコンセンサスアルゴリズムから複製プロトコルが導出された分散データベースであるMongoDBで設計され,実装された。TLA+で定式化され,TLA+証明システム(TLAPS)を用いて形式的に証明されたMongoRaftRe構成に対する誘導不変量を示した。また,MongoRaftRe構成の2つの重要な安全特性の形式的TLAPS証明,リーダCompletenesとStateMachineSafetyを提示した。著者らの知る限り,これらはRaftベースの複製システムのための動的再構成プロトコルの帰納的不変量と安全性証明をチェックした最初の機械である。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 安全性 ,  複製 ,  定理証明 ,  不変量 ,  *プロトコル ,  定式化 ,  *検証 ,  分散データベース
準シソーラス用語： 形式的検証 ,  *動的再構成 ,  分散システム ,  コンセンサスアルゴリズム , 【Automatic Indexing@JST】

著者キーワード (6件)： 分散システム ,  動的再構成 ,  形式的検証 ,  ラフト ,  TLA+ ,  定理証明

分類 (2件)： データ保護  (JD01020V) ,  計算理論  (JB02000A)

タイトルに関連する用語 (3件)： 動的再構成 ,  プロトコル ,  形式的検証