Grunnleggende konsepter
非信頼性ブロードキャスト通信を扱うためのセッション型システムを提案する。セッション型システムにより、プロトコルの実装を型チェックによって検証できる。
Sammendrag
本論文では、非信頼性ブロードキャスト通信のためのUnreliable Broadcast Session Calculus (UBSC)を提案する。UBSCは、非信頼性ブロードキャストと収集の2つの一般的な操作をセッション型で捉える。
メッセージの損失により、セッションエンドポイントが同期しなくなる可能性がある。そのため、UBSCはセッションエンドポイントの自律的な回復メカニズムを提供する。
型システムは、同期されたセッションエンドポイント間の安全性と進捗を保証する。また、Paxosコンセンサスプロトコルの実装を示すことで、UBSCの表現力を実証する。
Statistikk
非信頼性ブロードキャスト通信では、メッセージが失われる可能性がある
セッションエンドポイントが同期しなくなる可能性がある
自律的な回復メカニズムが必要である
Sitater
"Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking."
"We introduce the Unreliable Broadcast Session Calculus, a process calculus with unreliable broadcast communication, and equip it with a session type system that we show is sound."
"To cope with these cases, the semantics of the calculus offer flexible recovery mechanisms that follow the practice of ad-hoc and sensor networks."