Loading article…
到達可能性解析は、分散システムという特定の状況における到達可能性問題に対する解決策です。これは、メッセージの交換によって通信する一定数のローカルエンティティから構成される分散システムが、どのグローバル状態に到達できるかを判断するために使用されます。
到達可能性解析は、通信プロトコルの解析と検証のために1978年の論文で導入されました。[ 1 ]この論文は、プロトコルエンティティの有限状態モデリングを使用して交互ビットプロトコルを提示し、以前に説明した同様のプロトコルに設計上の欠陥があることを指摘した、1968年のBartlettらの論文[2]に触発されたものです。このプロトコルはリンク層に属し、特定の仮定の下で、メッセージの破損や損失が時折発生するにもかかわらず、損失や重複のない正しいデータ配信をサービスとして提供します。
到達可能性分析では、ローカルエンティティは状態と遷移によってモデル化されます。エンティティは、メッセージを送信したり、受信したメッセージを消費したり、ローカルサービスインターフェースでインタラクションを実行したりすると状態が変化します。グローバル状態 n個のエンティティを持つシステムの[ 3 ]は状態によって決定される。 エンティティの (i=1, ... n) と通信の状態最も単純なケースでは、2 つのエンティティ間の媒体は、転送中のメッセージ (送信済みだがまだ消費されていないメッセージ) を含む、反対方向の 2 つの FIFO キューによってモデル化されます。到達可能性分析では、エンティティのすべての可能な状態遷移シーケンスと、それに対応する到達したグローバル状態を分析することにより、分散システムの可能な動作を考慮します。[ 4 ]
到達可能性分析の結果は、分散システムの初期グローバル状態から到達可能なすべてのグローバル状態と、ローカルエンティティによって実行される送信、消費、およびサービスインタラクションのすべての可能なシーケンスを示すグローバル状態遷移グラフ（到達可能性グラフとも呼ばれる）です。ただし、多くの場合、この遷移グラフは無制限であり、完全に探索することはできません。遷移グラフは、プロトコルの一般的な設計上の欠陥をチェックするために使用できます（下記参照）が、エンティティによるサービスインタラクションのシーケンスがシステムのグローバルサービス仕様で与えられた要件に対応していることを検証するためにも使用できます。[ 1 ]
有界性:グローバル状態遷移グラフは、転送中のメッセージの数が有界であり、すべてのエンティティの状態数が有界である場合に有界である。有限状態エンティティの場合にメッセージの数が有界のままであるかどうかという問題は、一般には決定不可能である。[ 5 ]通常、転送中のメッセージの数が所定の閾値に達したときに、遷移グラフの探索を打ち切る。
以下は設計上の欠陥です。
例として、最初の図に示すように、メッセージma、mb、mc、mdを相互に交換する 2 つのプロトコル エンティティのシステムを考えます。プロトコルは、2 つのエンティティの動作によって定義され、それは 2 番目の図に 2 つの状態機械の形で示されています。ここで、記号 "!" はメッセージを送信することを意味し、"?" は受信したメッセージを消費することを意味します。初期状態は状態 "1" です。
3 番目の図は、このプロトコルの到達可能性分析の結果をグローバル状態機械の形で示しています。各グローバル状態は、プロトコルエンティティ A の状態 (左)、エンティティ B の状態 (右)、および中央にある転送中のメッセージ (上部: A から B へ、下部: B から A へ) の 4 つのコンポーネントで構成されています。このグローバル状態機械の各遷移は、プロトコルエンティティ A またはエンティティ B の 1 つの遷移に対応します。初期状態は [1, - - , 1] (転送中のメッセージなし) です。
この例では、グローバル状態空間が限定されていることがわかります。同時に転送されるメッセージの最大数は 2 つです。このプロトコルにはグローバルデッドロックがあり、それは状態 [2, - - , 3] です。状態 2 の A がメッセージmb を消費するための遷移を削除すると、グローバル状態 [2, ma mb ,3] と [2, - mb ,3]で未指定の受信が発生します。
プロトコルの設計は、基盤となる通信媒体の特性、通信相手が障害を起こす可能性、およびエンティティが消費する次のメッセージを選択するために使用するメカニズムに合わせて調整する必要があります。リンクレベルのプロトコルで使用される通信媒体は通常信頼性が低く、誤った受信やメッセージの損失（媒体の状態遷移としてモデル化される）が発生する可能性があります。インターネットIPサービスを使用するプロトコルは、順不同配信の可能性にも対処する必要があります。上位レベルのプロトコルは通常、セッション指向のトランスポートサービスを使用します。これは、媒体が任意のエンティティペア間でメッセージの信頼性の高いFIFO伝送を提供することを意味します。ただし、分散アルゴリズムの分析では、多くの場合、エンティティが完全に障害を起こす可能性が考慮されます。これは通常、期待されるメッセージが到着しない場合にタイムアウトメカニズムによって検出されます（媒体でのメッセージの損失と同様） 。
複数のメッセージが到着し、消費準備が整っている場合に、エンティティが消費する特定のメッセージを選択できるかどうかについては、さまざまな仮定がなされてきました。基本的なモデルは以下のとおりです。
未指定受信の問題を特定した最初の論文[ 6 ]と、その後の多くの研究は、単一の入力キューを想定していました。[ 7 ]未指定受信は、競合状態によって引き起こされることがあります。競合状態とは、2 つのメッセージが受信され、その順序が定義されていない状態です (これは、異なるパートナーからメッセージが来た場合によく起こります)。複数のキューまたは受信プールを使用すると、これらの設計上の欠陥の多くが解消されます。[ 8 ]受信プールを体系的に使用すると、到達可能性分析で部分的なデッドロックと (エンティティによって消費されずに) プールに永久に残るメッセージがチェックされるはずです。[ 9 ]
プロトコルモデリングに関する研究のほとんどは、分散エンティティの動作をモデル化するために有限状態機械（FSM）を使用しています（ 「有限状態機械の通信」も参照）。しかし、このモデルはメッセージパラメータやローカル変数をモデル化するには十分な機能を持っていません。そのため、 SDLやUMLステートマシンなどの言語でサポートされているような、いわゆる拡張FSMモデルがよく使用されます。残念ながら、このようなモデルでは到達可能性解析がはるかに複雑になります。
到達可能性解析の実際的な問題として、いわゆる「状態空間爆発」があります。プロトコルの 2 つのエンティティがそれぞれ 100 個の状態を持ち、媒体が各方向に最大 2 種類のメッセージを含む 10 種類のメッセージを持つ場合、到達可能性グラフのグローバル状態の数は 100 x 100 x (10 x 10) x (10 x 10) という 1 億という数に制限されます。そのため、到達可能性グラフ上で到達可能性解析とモデル検査を自動的に実行するためのツールが数多く開発されています。ここでは、SPIN モデルチェッカーと分散プロセスの構築と解析のためのツールボックスの 2 つの例のみを挙げます。
{{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）