モデル変換ルール集合の作成

モデル変換ルールの記述には，2.2.3に示したQVToを用いた．QVToは命令型言語の 一種であり，メタモデル間の変換を手続き的に記述することができる．

図4.5に，図 4.1における“Pthreads”ルールの記述の一部を例として示す．モデル変 換ルールconvertToPthreadFunctionReferenceは，Pthreadsライブラリに関係する関 数呼び出し識別し，抽象プログラムメタモデルで定義された関連する要素に変換し，関 数宣言を対応する要素に変換するものである．本モデル変換ルールの仮引数は，関数呼 び出しFunctionCallクラスのfunctionオブジェクトである．FunctionCallは，抽象 プログラムメタモデルで定義された要素の一つであり，関数呼び出しを意味する要素で あった．QVToではswitch文を用いることができ，function.getName()で得られる文 字列，すなわち，呼び出される関数の名前による分岐を定義している．例えば，関数名が

pthread_createである場合には，この関数呼び出しを，プロセスの実行を意味する抽象

プログラムメタモデルの論理要素の一つであるProcessRunnningFunctionReferenceオ ブジェクトに変換する．ここでは記載していないが，pthread_create関数呼び出しの引 数については，別途ProcessRunnningFunctionReferenceオブジェクトの引数への変換 を行っている．

QVToでは手続き的な記述が可能であるため，上記に示した例よりも，複雑な変換アル ゴリズムを定義することもできる．例えば，表4.1に示した“型宣言の最適化”ルールは，

抽象プログラムモデルをたどり定数を判別した上で，値の代入関係を解析し変数の取りう る値の最大値および最小値を見積もることで，変数の値域に関して探索範囲を縮退するよ うな変換を行う．

図4.5: QVToによるモデル変換ルール記述の例

表4.1に作成した抽象化に関わるモデル変換ルール集合の例を示す．ルールの種類の列 には，図3.4で示した，基本変換，ドメイン特化変換，タスク特化変換との対応を示した．

抽象化の種類の列には，ルールを意味論の変換と抽象化に分類した．名称の列には，ルー ルによる変換内容を示す名称を説明用に与えた．概説列に，各ルールの変換内容を概説 した．

表4.2に，本研究で作成した変換ルール集合により，C言語のコードがどのようにPromela コードに変換されるかについて代表的なものを示す．ただし，変換ルール集合により変換 が定義されるものである．POM/MCの変換能力がこれに限定されるものではなく，また，

異なる変換方針に基づく変換ルール集合を定義することもできる．POM/MCの構文解析 はC言語コンパイラフレームワークであるLLVM[34]の構文解析機能を利用しており，任 意のC言語プログラムを解析して実装モデルにASGを格納できる．実装モデルを抽象プ ログラムモデルに変換する際に，変換ルール集合に定義された情報のみがプログラムモデ ルに格納され，さらに抽象プログラムの情報が抽象化される．その結果が表4.2であり，

Promelaに変換可能なC言語プログラムの要素と変換方針は変換ルール集合により変更可

能である．

表4.1: モデル変換ルール集合の例 ル ー ル の 種

類

抽 象 化 の 種 類

名称 概説

基本 意 味 論 の 変 換

式の展開 代入や関数呼び出しなどC言語で入れ子に なった式を展開する．(例)a= (b=c)→ b=c;a=b;

多次元配列の分 解

C言語における多次元配列を一次元の配列 をフィールドに持つ構造体に分解する．

ポインタのエイ リアス解析

ポインタ参照の変化を解析し，ポインタに よる参照先データ参照を実体の参照に置き 換える．(例) int i,∗j;j = &i;∗j = 5; → int i;i= 5;

ド メ イ ン 特 化

Pthreads POSIXスレッドライブラリ(Pthreads)の 提供するスレッド生成や排他制御の機構を，

Promelaのプロセスやガード機構に置き換

える．

状態機械ドライ バ

このルールの引数で指定された関数を周期 的に呼ばれる構造に置き換え，状態遷移設 計を再現する．

タスク特化 エントリポイン ト

こ の ル ー ル の 引 数 で 指 定 さ れ た 関 数 を Promelaの初期プロセス(init)に指定する スタブ 指定された関数をスタブで置き換える．以 下の４種類のスタブをサポートしている．

(1) 機能を持たないスタブ (2) 定数を返す スタブ (3)指定された値域内のランダムな 値を返すスタブ(4)別途指定されたモデル コードを呼ぶスタブ

表明 指定されたソースコード中のラベルへのジ ャンプを表明に置き換える

抽象化 型宣言の最適化 整数型で宣言された変数と関数について，

代入関係から最大値と最小値を決定し，そ の範囲を表現するのにより小さい型で十分 な場合には，より小さい型に変更する．

未使用宣言の削 除

ドライバから利用されている宣言を再帰的 に求め，使われていない宣言を削除する．

表 4.2: POM/MCにおける代表的なC言語からPromelaへの変換

C言語要素 Promelaへの変換方針

関数 inline関数

関数引数 inline関数引数

関数返値 inline関数引数

main関数 initプロセス(main以外のスタートポイントも指定可能)

変数宣言 変数宣言(Promelaがサポートする型に限る)

構造体 構造データ型

配列 配列

多次元配列  構造データ型の配列

if if

for do

while if

ポインタ参照 参照先の実体の参照(静的に参照解決できる場合に限る)

代入 代入

入れ子の代入 複数文での代入

ƃ–‡’Žƒ–‡‡š’”‡••‹‘‘–”‹‰ſ‡š’śš’”‡••‹‘ƀƄ

ƃ‹ˆſ‡š’Ŝ‘…Ž•†‡ˆ‹‡†ſƀƀƄʴʴʴ†‡ˆ‹‡†š’”‡••‹‘ʳʳʳ ƃ‡Ž•‡‹ˆ ſ‡š’ ʰ—ŽŽƀƄʴʴʴ—ŽŽš’”‡••‹‘ʳʳʳ

ƃ‡Ž•‡‹ˆ ſ‡š’Ŝ‘…Ž•˜ƒŽ‹†ſƀƀƄʴʴʴ˜ƒŽ‹†š’”‡••‹‘ʳʳʳ

ƃ‡Ž•‡‹ˆ ſ‡š’Ŝ‘…Ž•‹†ˆſ—š’”‡••‹‘ƀƀƄ”—ƃ‡š’Ŝ‘…Ž•›’‡ſ—š’”‡••‹‘ƀŜ’”‘…‡••Ŝƒ‡ŵƄ ſƃ‡š’”‡••‹‘•‘–”‹‰ſ‡š’Ŝ‘…Ž•›’‡ſ—š’”‡••‹‘ƀŜƒ”‰—‡–•ƀŵƄƀ

ƃ‡Ž•‡‹ˆ ſ‡š’Ŝ‘…Ž•‹†ˆſ†‡–‹ˆ‹‡”ƀƀƄ

ƃ‹ˆſ‡š’Ŝ‘…Ž•›’‡ſ†‡–‹ˆ‹‡”ƀŜ†‡…Žƒ”ƒ–‹‘ʳʴ—ŽŽƒ†‘–‡š’Ŝ‘…Ž•›’‡ſ†‡–‹ˆ‹‡”ƀŜ

†‡…Žƒ”ƒ–‹‘Ŝ‘…Ž•˜ƒŽ‹†ſƀƀƄƃ‡š’Ŝ‘…Ž•›’‡ſ†‡–‹ˆ‹‡”ƀŜ†‡…Žƒ”ƒ–‹‘Ŝƒ‡ŵƄ ƃ‡Ž•‡Ƅʴʴʴ‹••‹‰†‡…Žƒ”ƒ–‹‘ſ†‡–‹ˆ‹‡”ƀʳʳʳƃŵ‹ˆƄ

ƃ‡Ž•‡‹ˆ ſ‡š’Ŝ‘…Ž•‹†ˆſ ‹‡Ž†……‡••ƀƀƄŝſ┬␎ƀŝ ƃ‡Ž•‡‹ˆ ſ‡š’Ŝ‘…Ž•‹†ˆſ‘•–ƒ–ƀƀƄ ŝſ┬␎ƀŝ

ƃ‡Ž•‡‹ˆ ſ‡š’Ŝ‘…Ž•‹†ˆſ‡•‡”˜‡†ƒ”‹ƒ„Ž‡ƀƀƄ ŝſ┬␎ƀŝ ƃ‡Ž•‡‹ˆ ſ‡š’Ŝ‘…Ž•‹†ˆſ””ƒ›……‡••ƀƀƄ ŝſ┬␎ƀŝ

ŝſ┬␎ƀŝ ƃŵ‹ˆƄ ƃŵ–‡’Žƒ–‡Ƅ

図 4.6: M2Tテンプレートの例