Основні поняття
分散システムのオフラインランタイム検証において、部分観測とマルチプレフィックスの重要性を強調。
Анотація
本コンテンツは、分散システムにおけるオフラインランタイム検証の重要性と、部分観測やマルチプレフィックスの考え方を探求しています。複数のローカルトレースからなるマルチトレースを解析する際に生じる問題点やアルゴリズムについて詳細に説明されています。特に、部分観測がもたらす情報欠落やマルチプレフィックスという概念が焦点となっています。
Статистика
マルチトレースは複数のローカル実行トレースから成り立つ。
部分観測では全体像が把握できず、情報欠落が発生する可能性がある。
マルチプレフィックスはマルチトレースの接頭辞であり、完全なグローバルトレースを再現しないことがある。
オフラインランタイム検証アルゴリズムは部分観測やマルチプレフィックスを考慮して開発されている。
最終的な派生物が終了した場合、連結されたアクションは元々の相互作用の意味論に属することを示す。
Цитати
"Runtime Verification (RV) refers to a family of techniques in which system executions are observed and confronted to formal specifications, with the aim of identifying faults."
"In Offline RV, observation is done in a first step and verification in a second step, on a static artifact collected during the observation."
"A major challenge in analyzing multi-traces is that there are no practical means to synchronize the ends of observations of all the local traces."
"We address this via an operation, called lifeline removal, which we apply on-the-fly on the specification during the verification of a multi-trace once a local trace has been entirely analyzed."
"This may allow further execution of the specification via removing deadlocks due to the partial orders of actions."