プロメラ

PROMELA (プロセスまたはプロトコルメタ言語) は、 Gerard J. Holzmannによって導入された検証 モデリング言語です。この言語を使用すると、たとえば分散システムをモデル化するために、並行プロセスを動的に作成できます。 PROMELA モデルでは、メッセージチャネルを介した通信を同期 (ランデブー) または非同期 (バッファリング) として定義できます。 PROMELA モデルは、SPIN モデルチェッカーを使用して分析し、モデル化されたシステムが目的の動作を生成することを検証できます。コンピュータ支援検証 (CAVA) プロジェクトの一環として、Isabelle/HOLを使用して検証された実装も利用できます。 ^{[1] [2] Promela で作成されたファイルには、伝統的に}ファイル拡張子が付けられます。 .pml

PROMELA は、並列システムのロジックを検証することを目的としたプロセスモデリング言語です。PROMELA のプログラムが与えられると、Spin はモデル化されたシステムの実行のランダムまたは反復シミュレーションを実行してモデルの正しさを検証したり、システム状態空間の高速で徹底的な検証を実行するCプログラムを生成することができます。シミュレーションと検証中、SPIN はデッドロック、未指定の受信、および実行不可能なコードが存在しないかどうかをチェックします。この検証ツールは、システム不変条件の正しさを証明するためにも使用でき、非進行実行サイクルを検出できます。最後に、Promela の never-claims を使用するか、または制約を時相論理で直接定式化することにより、線形時間の時相制約の検証をサポートします。各モデルは、環境に関するさまざまなタイプの仮定の下で SPIN を使用して検証できます。SPIN を使用してモデルの正しさが確立されると、その事実は、後続のすべてのモデルの構築と検証に使用できます。

PROMELA プログラムは、プロセス、 メッセージ チャネル、および 変数で構成されます。プロセスは、分散システムの同時実行エンティティを表すグローバル オブジェクトです。メッセージ チャネルと変数は、プロセス内でグローバルまたはローカルに宣言できます。プロセスは動作を指定し、チャネルとグローバル変数はプロセスが実行される環境を定義します。

PROMELA で使用される基本的なデータ型を以下の表に示します。ビット単位のサイズは PC i3​​86/Linux マシン用です。

bitとbool という名前は、1 ビットの情報の同義語です。byteは、0 から 255 までの値を格納できる符号なしの量です。shortとintは、格納できる値の範囲のみが異なり、符号付きの量です。

変数は配列として宣言することもできます。たとえば、次の宣言があります。

 整数x [ 10 ];  

次のような配列添字式でアクセスできる 10 個の整数の配列を宣言します。

x[0] = x[1] + x[2];

ただし、配列は作成時に列挙できないため、次のように初期化する必要があります。

 int x [ 3 ]; x [ 0 ] = 1 ; x [ 1 ] = 2 ; x [ 2 ] = 3 ; 
   
   
   

配列のインデックスは、一意の整数値を決定する任意の式にすることができます。範囲外のインデックスの効果は未定義です。多次元配列は、typedef構造を使用して間接的に定義できます (以下を参照)。

変数またはメッセージ チャネルの状態は、プロセスによってのみ変更または検査できます。プロセスの動作は、proctype宣言によって定義されます。たとえば、次の例では、1 つの変数状態を持つプロセス タイプA を宣言しています。

プロシージャタイプA()
 {
     バイト状態;
     状態 = 3;
 }

proctype定義はプロセスの動作を宣言するだけで、実行はしません。 最初は、PROMELA モデルで 1 つのプロセスだけが実行されます。これは、すべての PROMELA 仕様で明示的に宣言する必要がある initタイプのプロセスです。

新しいプロセスは、 proctypeの名前からなる引数を取るrunステートメントを使用して生成できます。この引数からプロセスがインスタンス化されます。 run演算子は、初期プロセスだけでなく、 proctype定義の本体でも使用できます。これにより、PROMELA でプロセスを動的に作成できます。

実行中のプロセスは、終了すると消えます。つまり、 proctype定義の本体の最後まで到達し、そのプロセスによって開始されたすべての子プロセスが終了すると消えます。

proctype もアクティブになる場合があります(下記)。

中括弧で囲まれた一連のステートメントの前にキーワードatomicを付けることにより、ユーザーは、そのシーケンスが他のプロセスとインターリーブされずに 1 つの分割できない単位として実行されることを示すことができます。

原子
 {
     声明;
 }

アトミック シーケンスは、検証モデルの複雑さを軽減する上で重要なツールとなります。アトミック シーケンスは、分散システムで許可されるインターリーブの量を制限することに注意してください。扱いにくいモデルは、ローカル変数のすべての操作にアトミック シーケンスのラベルを付けることで扱いやすくすることができます。

メッセージ チャネルは、あるプロセスから別のプロセスへのデータ転送をモデル化するために使用されます。これらは、次のようにローカルまたはグローバルに宣言されます。

ちゃん qname = [16] の {short}

これは、最大 16 個のshortタイプのメッセージを保存できるバッファ チャネルを宣言します(ここでは容量は 16)。

声明:

qname ! 式;

式exprの値をqnameという名前のチャネルに送信します。つまり、値をチャネルの末尾に追加します。

声明:

qname ? メッセージ;

メッセージを受信し、チャネルの先頭から取得して、変数 msg に格納します。チャネルは先入れ先出しの順序でメッセージを渡します。

ランデブー ポートは、ストア長が 0 のメッセージ チャネルとして宣言できます。たとえば、次のようになります。

chan ポート = [0] / {byte}

バイトタイプのメッセージを渡すことができるランデブー ポートを定義します。このようなランデブー ポートを介したメッセージのやり取りは、定義上は同期的です。つまり、送信者または受信者 (チャネルに最初に到着したもの) は、 2 番目に到着する競合者(受信者または送信者) をブロックします。

バッファリングされたチャネルが容量いっぱいになると (送信は受信入力より「容量」数だけ先の出力です)、チャネルのデフォルトの動作は同期になり、送信者は次の送信をブロックします。チャネル間で共有される共通のメッセージ バッファがないことに注意してください。チャネルを単方向およびポイント ツー ポイントとして使用する場合と比較して、複雑さが増しますが、複数の受信者または複数の送信者間でチャネルを共有し、独立したデータ ストリームを 1 つの共有チャネルにマージすることができます。このことから、1 つのチャネルを双方向通信に使用することもできます。

PROMELA には 3 つの制御フロー構造があります。それらは、ケース選択、繰り返し、無条件ジャンプです。

最も単純な構造は選択構造です。たとえば、 2 つの変数aとbの相対値を使用して、次のように記述できます。

もし
 :: (a != b) -> オプション1
 :: (a == b) -> オプション2
 フィ

選択構造には 2 つの実行シーケンスが含まれており、それぞれの先頭には二重コロンがあります。リストから 1 つのシーケンスが実行されます。シーケンスは、最初のステートメントが実行可能である場合にのみ選択できます。制御シーケンスの最初のステートメントはガードと呼ばれます。

上記の例では、ガードは相互に排他的ですが、必ずしもそうである必要はありません。複数のガードが実行可能な場合、対応するシーケンスの 1 つが非決定的に選択されます。すべてのガードが実行不可能な場合、プロセスはガードの 1 つを選択できるようになるまでブロックされます。(逆に、実行可能なガードがない場合、 occam プログラミング言語は停止するか、続行できなくなります。)

もし
 :: (A == true) -> オプション1;
 :: (B == true) -> option2; /* A==true の場合もここに到達する可能性があります */
 :: そうでない場合は、 fallthrough_option;
 フィ

非決定論的な選択の結果、上記の例では、A が真であれば、両方の選択肢が取られる可能性があります。「従来の」プログラミングでは、if – if – else構造を順番に理解します。ここで、if – 二重コロン – 二重コロンは、「いずれか 1 つが準備完了」と理解する必要があり、準備ができていない場合にのみ elseが取られます。

もし
 :: 値 = 3;
 :: 値 = 4;
 フィ

上記の例では、値 3 または 4 が非決定的に与えられます。

ガードとして使用できる疑似ステートメントには、タイムアウトステートメントとelseステートメントの 2 つがあります。タイムアウトステートメントは、プロセスが決して真にならない可能性のある条件の待機を中止できるようにする特別な条件をモデル化します。else ステートメントは、選択ステートメントまたは反復ステートメントの最後のオプション シーケンスの最初のステートメントとして使用できます。else は、同じ選択内の他のすべてのオプションが実行可能でない場合にのみ実行可能です。また、else はチャネルと一緒に使用できません。

選択構造の論理的な拡張は繰り返し構造です。例:

する
 :: カウント = カウント + 1
 :: a = b + 2
 :: (カウント == 0) -> ブレーク
 od

PROMELA の繰り返し構造を説明します。一度に選択できるオプションは 1 つだけです。オプションが完了すると、構造の実行が繰り返されます。繰り返し構造を終了する通常の方法は、breakステートメントを使用することです。これにより、繰り返し構造の直後の命令に制御が移ります。

ループを中断する別の方法は、gotoステートメントです。たとえば、上記の例を次のように変更できます。

する
 :: カウント = カウント + 1
 :: a = b + 2
 :: (count == 0) -> 完了へ
 od
 終わり：
 スキップ;

この例のgotoはdone というラベルにジャンプします。ラベルはステートメントの前にのみ配置できます。たとえば、プログラムの最後にジャンプするには、ダミー ステートメントskipが便利です。これは常に実行可能で効果のないプレースホルダーです。

PROMELA の重要な言語構成要素で、少し説明が必要なのがassertステートメントです。次の形式のステートメント:

アサート(任意のブール条件)

常に実行可能です。指定されたブール条件が満たされる場合、文は効果がありません。ただし、条件が必ずしも満たされない場合、文はSPINによる検証中にエラーを生成します。

PROMELA のtypedef定義は、定義済みまたは以前に定義された型のデータ オブジェクトのリストに新しい名前を導入するために使用できます。新しい型名は、新しいデータ オブジェクトを宣言してインスタンス化するために使用できます。これは、あらゆるコンテキストで明白な方法で使用できます。

 typedef MyStruct { shortフィールド1 ; byteフィールド2 ; }; 
 
      
      
 

typedef構造で宣言されたフィールドへのアクセスは、C プログラミング言語と同じ方法で行われます。例:

私の構造体x;
フィールド1 = 1;

変数xのフィールドField1に値1を割り当てる有効な PROMELA シーケンスです。

activeキーワードは、任意のproctype定義の前に付けることができます。キーワードが存在する場合、その proctype のインスタンスは、初期システム状態でアクティブになります。キーワードのオプションの配列サフィックスを使用して、その proctype の複数のインスタンス化を指定できます。例:

アクティブ proctype A() { ... }
 アクティブ [4] proctype B() { ... }

実行可能性のセマンティクスは、Promela でプロセス同期をモデル化するための基本的な手段を提供します。

mtype = {M_UP、M_DW};
 chan Chan_data_down = [0] の {mtype};
 chan Chan_data_up = [0] の {mtype};
 proctype P1 (chan Chan_data_in、Chan_data_out)
 {
     する
     :: Chan_data_in ? M_UP -> スキップ;
     :: Chan_data_out ! M_DW -> スキップ;
     od;
 };
 proctype P2 (chan Chan_data_in、Chan_data_out)
 {
     する
     :: Chan_data_in ? M_DW -> スキップ;
     :: Chan_data_out ! M_UP -> スキップ;
     od;
 };
 初期化
 {
     原子
     {
         P1 (Chan_data_up、Chan_data_down) を実行します。
         P2 (Chan_data_down、Chan_data_up) を実行します。
     }
 }

この例では、2 つのプロセス P1 と P2 には、(1) 他方からの入力、または (2) 他方への出力という非決定的な選択肢があります。2 つのランデブー ハンドシェイクが可能 (実行可能) であり、そのうちの 1 つが選択されます。これは永久に繰り返されます。したがって、このモデルではデッドロックは発生しません。

Spin が上記のようなモデルを分析する場合、非決定論的アルゴリズムで選択肢を検証し、実行可能な選択肢をすべて調べます。ただし、Spin のシミュレーターが検証されていない可能性のある通信パターンを視覚化する場合、ランダムジェネレーターを使用して「非決定論的」な選択肢を解決することがあります。そのため、シミュレーターは不正な実行を表示できない場合があります (例では、不正な痕跡はありません)。これは、検証とシミュレーションの違いを示しています。さらに、Refinement を使用して Promela モデルから実行可能なコードを生成することもできます。^[3]

次の識別子はキーワードとして使用するために予約されています。

• スピンホームページ
• Spin チュートリアルとオンライン リファレンス
• 簡潔な Promela リファレンス
• オートマトンによるコンピュータ支援検証：「CAVAプロジェクト」（2010-2019）および「検証済みモデルチェッカー」（2016年現在）のウェブサイト