POM/MC の評価実験

POM/MCを用いてC言語ソースコードからPromelaモデルを抽出しモデル検査を実

施できることを確認するため，いくつかのサンプルプログラムについて評価実験を行った．

表4.3に，各サンプルプログラムに対して，モデル抽出とモデル検査を実施した結果を示 す．分類にSVCOMPとあるプログラムは，キュープログラムも含め，SVCOMPのベン チマークとして公開されているソースコードである．分類にオリジナルとあるプログラム は，筆者らが評価用に作成したプログラムである．いずれも，Pthreadsライブラリを用い て，複数のスレッドが並行して動作するプログラムである．以下では，本論文の例題とし

3http://www.eclipse.org/m2m/, 2012-06-01

表4.3: ケーススタディのまとめ

分類  プログラム名 C (LOC) Promela (LOC) シンボル数

SVCOMP test lock 14.BUG.c 163 353 32

queue BUG.c 157 215 40

twostage 3 BUG.c 111 190 30

fib bench BUG.c 31 97 18

オリジナル 哲学者問題 104 203 175 座席予約システム 495 599

て用いたキュープログラムと，より実システムに類似した構造を持つ座席予約システムを 用いた評価実験の結果について述べる．

4.6.1 キュープログラム

付録A.1にキュープログラムのC言語ソースコードを，付録A.2にPOM/MCによっ て抽出したPromelaコードを掲載した．また，付録B.1には，C言語モデルから抽象プ ログラムモデルへの変換を定義する変換ルールの例を，付録B.3には，抽象プログラムモ デル上での変換を定義する変換ルールの例を，付録B.2には，抽象プログラムモデルから

Promelaモデルへの変換の例を掲載した．このような変換ルールを作成することで，C言

語からPromelaへの変換と，モデル検査が可能であることを確認した．

4.6.2 座席予約システム

キュープログラムより現実のシステムに近い例として，簡単な座席予約システムを模擬 するC言語プログラムを作成した．これに対して，POM/MCを用いてモデル抽出とモデ ル検査を行った．

座席予約システムの概説

このプログラムは，座席の予約を管理する一つのサーバーと，予約を行う複数のクライ アントからなる．クライアントからサーバーへは，指定した席の空き状況を問い合わせる

“checking availability”，指定した席の予約をリクエストする“reservation”，指定した席 の予約確認を行う“confirmation”メッセージを送る．サーバーは，各メッセージに対して，

空き状況の有無，予約可否，予約状況を返す．このプログラムには，ダブルブッキングを 起こす問題が含まれている．

複数のクライアントから同時に“checking availability”メッセージを受けた場合，すべ てのクライアントに予約可能と返してしまうためである．

このプログラムでは，クライアント-サーバーシステムの並行動作を実現するため，Pthreads ライブラリを用い，サーバーとクライアントは各々がスレッドとして動作する．

void* terminal_thread(int

*id){

...

} ...

for (i = 0;

i < MAX_TERMINALS; i++) { pthread_create(

&terminals[i], NULL, terminal_thread, (void *)i);

}

proctype terminal_thread (int id) { ...

} ...

i = 0;

do

::(i < MAX_TERMINALS)->

run terminal_thread(i);

i++;

::else->

break od

C source code Promela model code

:FunctionDecl name=terminal_thread

:CompoundStmt :ParameterDecl

:IterationStmt

:CompoundStmt

:ExpStmt :ExpStmt :AssgnmentExp :FunctionCall

:FunctionRef

:AddressReference :Identifier

Name=terminal_thread :FunctionRef

:AssignmentExp :BinaryOp :IncrementExp

:FunctionDecl name=pthread_create :ReferenceTypeSpec

:Identifier name=pthread_create

:ArrayAccess

:ProcessFunctionDecl name=terminal_thread

:CompoundStmt :ParameterDecl

:IterationStmt

:CompoundStmt

:ExpStmt :ExpStmt :AssgnmentExp :FunctionCall

:ProcessRunning-FunctionRef :AddressReference

:Identifier name=terminal_thread :FunctionRef

:AssignmentExp :BinaryOp :IncrementExp :ReferenceTypeSpec

:Identifier name=pthread_create

:ArrayAccess Abstract program model

図 4.8: Pthreadsライブラリ利用の抽象化

モデル変換ルールによる変換の例

本節では，座席予約システムのケースで用いたモデル変換の例として，Pthreadsライブ ラリが提供する関数と型の利用を，Promela言語の並行プロセスで実現するため変換につ いて解説する．また，スレッド間の通信の変換についても概説する．

図4.8に，モデル変換の手順を示す．元となるC言語ソースコードと対応するPromela コード，それらを橋渡しする抽象プログラムモデルを示している．C言語モデルと，Promela モデルは，各コードと対応しているため，ここでは省略する．

4.4.1節で述べたように，C言語のpthread_create関数は，Promelaのrun文に対応 する．また，C言語の関数宣言は，Promelaのproctype宣言に対応するものである．

pthread_creat関数に対応するFunctionCallオブジェクトを参照しているFunctionRef オブジェクトを，ProcessRunnigFunctionRefオブジェクトに置き換えている．抽象プロ グラムモデルからPromelaモデルへの変換により，ProcessRunnigFunctionRefオブジェ クトはPromelaのrun文の要素に対応づく．これにより，pthread_creat関数は，run文 に変換されることになる．

また，ProcessRunnigFunctionRefオブジェクトが参照している関数は，ProcessFunctioDecl オブジェクトに変換される．ProcessFunctioDeclオブジェクトは，Promelaのproctype 宣言に対応づく．これにより，pthread_creat関数の引数であるスレッド関数の宣言は，

PromelaのProctype宣言に変換されることになる．このようにして，pthread_creat関 数によるスレッド生成が，run文によるプロセス生成に変換できる．

次に，通信の変換について説明する．座席予約システムの実装では，クライアントと サーバー間の通信を行うメッセージ関数として，送信を行うchan_send関数，受信を行う chan_recieve関数，初期化を行うchan_init関数を作成した．また，メッセージキュー

を実現する構造体struct型であるchan_sを定義した．

例えば，chan_send関数の呼び出しを示すFunctionCallオブジェクトを参照するFunctionRef オブジェクトは，論理要素であるMessageSenfingFunctionRefオブジェクトに対応づけ る．抽象プログラムモデル上の論理要素とPromelaの言語要素の対応を定義することで，

MessageSenfingFunctionRefオブジェクトを“!”演算子による送信文に対応づける．こ れにより，chan_send関数の呼び出しは，“!”演算子による送信文に変換できる．受信を 行うchan_recieve関数についても，他のメッセージ関数も同様である．

これらの言語間の意味論の変換を行うモデル変換ルール集合のほか，状態爆発を防ぐこ とを目的に以下のルールを定義した．

• 座席数を示す定数の値を変更する

• 一括して同じ処理を繰り返すループ（例えば，座席予約情報の初期化）をループの ない処理に変更する

結果

準備したモデル変換ルールを用いることで，Promelaモデルを抽出することができた．

抽出されたPromelaモデルは約700行であった．また，モデル検査によって，ダブルブッ キング問題を再現できた．