プロメラ
Verification modeling language

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

導入

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

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

言語リファレンス

データ型

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

名前 サイズ（ビット） 使用法 範囲
少し 1 署名なし 0..1
ブール 1 署名なし 0..1
バイト 8 署名なし 0..255
mタイプ 8 署名なし 0..255
短い 16 署名 −2 15 ..2 15 − 1
整数 32 署名 −2 31 ..2 31 − 1

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を宣言しています。 

 proctype A () {バイト状態;状態= 3 ; }

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

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

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

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

原子構造

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

 アトミック
{ステートメント; }

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

メッセージパッシング

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

chan qname = [ 16 ]の{ short }

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

声明: 

qname ! 式;

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

声明: 

qname ? メッセージ;

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

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

チャネルポート= [ 0 ] / {バイト}

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

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

制御フロー構造

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

症例選択

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

 if 
:: ( a != b ) ->オプション1 :: ( a == b ) ->オプション2 fi

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

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

 if 
:: ( A == true ) -> option1 ; :: ( B == true ) -> option2 ; /* A==true の場合もここに到達する可能性があります */ :: else -> fallthrough_option ; fi

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

 if 
::値= 3 ; ::値= 4 ; fi

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

ガードとして使用できる擬似文は2つあります。timeout文とelse文です。timeout文は、決して真にならない可能性のある条件の待機をプロセスが中止できるようにする特別な条件をモデル化します。else文は、選択文または反復文における最後のオプションシーケンスの開始文として使用できます。else文は、同じ選択内の他のすべてのオプションが実行不可能な場合にのみ実行可能です。また、else文はチャネルと併用できません。

繰り返し（ループ）

選択構造の論理的拡張は繰り返し構造です。例えば： 

 do 
:: count = count + 1 :: a = b + 2 :: ( count == 0 ) -> break od

PROMELA における繰り返し構造を記述します。一度に選択できるオプションは 1 つだけです。オプションが完了すると、構造の実行が繰り返されます。繰り返し構造を終了するには、通常、break文を使用します。break 文は、繰り返し構造の直後の命令に制御を移します。

無条件ジャンプ

ループを中断するもう一つの方法は、goto文です。例えば、上記の例を次のように修正できます。 

 do 
:: count = count + 1 :: a = b + 2 :: ( count == 0 ) -> goto done od done : skip ;

この例のgotoはdone というラベルにジャンプします。ラベルは文の前にのみ記述できます。例えば、プログラムの末尾にジャンプするには、ダミー文skipが便利です。skip は常に実行可能で、効果を持たないプレースホルダです。

アサーション

PROMELA の重要な言語構成要素として、少し説明が必要なのがassert文です。次のような形式の文があります。 

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

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

複雑なデータ構造

PROMELAのtypedef定義は、定義済みまたは以前に定義された型のデータオブジェクトのリストに新しい名前を付けるために使用できます。新しい型名は、新しいデータオブジェクトの宣言とインスタンス化に使用でき、任意のコンテキストで明確に使用できます。 

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

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

私の構造体 x;
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 ] of { mtype }; chan Chan_data_up = [ 0 ] of { mtype }; proctype P1 ( chan Chan_data_in 、Chan_data_out ) { do :: Chan_data_in ? M_UP -> skip ; :: Chan_data_out ! M_DW -> skip ; od ; }; proctype P2 ( chan Chan_data_in 、Chan_data_out ) { do :: Chan_data_in ? M_DW -> skip ; :: Chan_data_out ! M_UP -> skip ; od ; }; init { atomic { run P1 ( Chan_data_up 、Chan_data_down ); run P2 ( Chan_data_down 、Chan_data_up ); } }

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

Spinは上記のようなモデルを解析する際に、非決定論的なアルゴリズムを用いて選択肢を検証し、実行可能な選択肢をすべて探索します。しかし、Spinのシミュレータは、検証されていない可能性のある通信パターンを視覚化する際に、乱数生成器を用いて「非決定論的な」選択肢を解決する場合があります。そのため、シミュレータは誤った実行結果を表示できない場合があります（この例では、誤った実行結果は存在しません）。これは、検証とシミュレーションの違いを示しています。さらに、Refinementを用いてPromelaモデルから実行可能なコードを生成することも可能です。[3]

キーワード

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

  • アクティブ
  • アサート
  • 原子
  • 少し
  • ブール
  • 壊す
  • バイト
  • ちゃん
  • d_ステップ
  • D_proctype
  • する
  • それ以外
  • 空の
  • 有効
  • フィ
  • 満杯
  • 後藤
  • 隠れた
  • もし
  • 列をなして
  • 初期化
  • 整数
  • レン
  • mタイプ
  • 空の
  • 一度もない
  • フル
  • od
  • の
  • pc_value
  • プリント
  • 優先度
  • プロトタイプ
  • 提供された
  • 走る
  • 短い
  • スキップ
  • タイムアウト
  • 型定義
  • ない限り
  • 署名なし
  • xr
  • xs

参考文献

  1. ^ Neumann, René (2014年7月17～18日). 「Promelaを用いた完全検証済み実行可能LTLモデルチェッカー」(PDF) . VSTTE: 検証済みソフトウェアに関するワーキングカンファレンス：理論、ツール、実験. LNCS . 第8471巻. ウィーン: Springer. pp.  105– 114. 2015年10月7日時点のオリジナル(PDF)からのアーカイブ。
  2. ^ CAVAプロジェクトのウェブサイト
  3. ^ Sharma, Asankhaya. 「Promelaの改良計算法」複雑系コンピュータシステムのエンジニアリング（ICECCS）、2013年第18回国際会議、IEEE、2013年。
  • Spinのホームページ
  • Spinチュートリアルとオンラインリファレンス
  • 簡潔な Promela リファレンス
  • オートマトンによるコンピュータ支援検証：「CAVAプロジェクト」（2010-2019）および「検証済みモデルチェッカー」（2016年以降）ウェブサイト
Retrieved from "https://en.wikipedia.org/w/index.php?title=Promela&oldid=1315898743"