SPINを用いたVDM仕様に対するモデル検査適用手法 Applying Model

୍⯡♫ᅋἲே 㟁Ꮚ᝟ሗ㏻ಙᏛ఍ ಙᏛᢏሗ‫ٻ‬
‫ٻڇڮڞڤکڪڭگڞڠڧڠٻڡڪٻڠگڰگڤگڮکڤٻڠڣگ‬
‫ٻۏۍۊۋۀڭٻۇڼھۄۉۃھۀگٻڠڞڤڠڤ‬
社団法人 電子情報通信学会
信学技報
‫ٻڮڭڠڠکڤڢکڠٻکڪڤگڜڞڤکڰڨڨڪڞٻڟکڜٻکڪڤگڜڨڭڪڡکڤ‬
‫ٻڄڒڋڈڐڌڋڍڃڒڍڈڐڌڋڍڠڮڝڦڇڏڎڈڐڌڋڍڮڮ‬
THE INSTITUTE OF ELECTRONICS,
TECHNICAL REPORT OF IEICE.
‫ ٻ‬INFORMATION AND COMMUNICATION ENGINEERS
SPIN を用いた VDM 仕様に対するモデル検査適用手法
林
信宏†
大森 洋一†
日下部
茂†
荒木啓二郎†
† 九州大学大学院システム情報科学研究院 〒 819–0395 福岡市西区元岡 744
E-mail: †{h-lin,yomori,kusakabe}@ait.kyushu-u.ac.jp, ††[email protected]
あらまし VDM (Vienna Development Method) は、形式手法の一つで，ソフトウェア開発の要求に対して様々な抽
象レベルの仕様記述が可能である．VDM あるいは形式仕様をソフトウェア開発に適用することは，高品質ソフトウェ
アに繋ぐ鍵である．しかし，VDM の適用から一番利益を得るためには，VDM 仕様の妥当性確認と検証 (validation
and veification, V&V) が重要である．本稿では，VDM における仕様アニメーションの機能を活用してモデル検査の
適用手法を提案する．この手法は，VDM 仕様アニメーションツール VDMJ とモデル検査ツール SPIN を持ち合わせ
してハイブリットモデルといった検証用モデルを築くことにより，SPIN を用いた VDM 仕様のモデル検査を実現する．
キーワード
VDM(Vienna Development Method)，モデル検査，SPIN
Applying Model Checking on VDM Models using SPIN
Hsin-Hung LIN† , Yoichi OMORI† , Shigeru KUSAKABE† , and Keijiro ARAKI†
† Faculty of Information Science and Electrical Engineering, Kyushu University
744 Motooka, Nishi-ku, Fukuoka, 819–0395 Japan
E-mail: †{h-lin,yomori,kusakabe}@ait.kyushu-u.ac.jp, ††[email protected]
Abstract The Vienna Development Method (VDM) is a formal method which supports modeling and analysis
of software systems at various levels of abstraction. Case studies have shown that applying VDM, or formal specification in general, in software development processes is the key of realizing high quality software development.
However, to derive full benefit from the use of VDM in software development, associative activities such as validating and verifying VDM models are crucial. Since the primary way for verifying a VDM model is testing by
specification animation, we aim to utilize the animation feature of VDM to apply model checking techniques. In
this paper, we propose an approach to support model checking VDM models by constructing a hybrid verification
model combining VDMJ, a VDM interpreter, and SPIN model checker.
Key words Vienna Development Method (VDM), Model Checking, SPIN
1. は じ め に
VDM (Vienna Development Method) [1]∼[3] は、形式手法
VDM++ [2] 仕様のスタイルをどうきめるか，及びテストケー
スをどう設計するかが力を一番入れたところである．
一方，並行性 (concurrency) や反応性 (reactivity) の持つシ
の一つであり，ソフトウェアの様々な抽象レベルでの仕様記述
ステムに対して，実行系列を注目する動的性質が重要であり，
が可能である．VDM モデル，あるいは VDM 仕様は，ソフト
事前事後条件及び不変条件を含める機能的仕様では不足がある．
ウェアの要求分析の結果を VDM 仕様記述言語（VDM-SL）で
これらの動的性質は，よく時相論理式で表現されていて，機能
記述した形式仕様であり，陰仕様または陽仕様の組合せで構成
的仕様の制約との繋がりが直接に見えにくくて，モデル検査 [8]
されている．
のような技術を導入する必要がある．
現場でのソフトウェア開発において仕様策定と設計段階に
現在 VDM 仕様の検証に使える主な手法はインタプリタによ
VDM を導入した実績がいくつかある [4]∼[6]．VDM を導入し
るアニメーションを用いたテストであり，モデル検査を適用す
た基本的な利点は，仕様の曖昧さを除去することで知らされて
る技術がない．我々は，仕様アニメーションを活用してモデル
いる．しかし，VDM の導入に一番利益を得るためには，VDM
検査技術を VDM 仕様の検証に適用しようと考え，ハイブリッ
仕様の妥当性確認と検証 (validation and veification, V&V)
ト検証モデルの構築法を提案する．具体的には，SPIN モデル
がとても重要である．例えば，FeliCa カードの開発 [7] では，
検査ツール [9] のモデリング言語 PROMELA に SPIN の組み
—1—
This article is a technical report without peer review, and its polished and/or extended version may be published elsewhere.
Copyright ©2015 by IEICE
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
module SIMPLE
exports all
definitions
types
myNat = nat
inv n == n in set {0,...,9};
オブジェクト指向のための拡張である．VDM-RT は VDM++
をさらにスレッドのスケジューリング及び時間に関する記述
で拡張した．本稿で提案する手法は，基本的に VDM-SL と
VDM++に適用できる．VDM-RT に適用することも可能だが，
時間とスケジューリングに関する対応が必要になる．
state S of
pool : set of myNat
init s == s = mk_S({0,4,9})
inv s == s <> mk_S({2,8}) /* two danger numbers */
end
operations
putintoS : set of myNat ==> set of myNat
putintoS(a) == ( pool := pool union a; return pool )
pre card a <= 2 and card a > 0
post card pool >= card pool~;
2. 2 SPIN
モデル検査 [8] はソフトウェアとハードウェアに対する有力な
検証技術である．モデル検査の基本アイデアは，システムの全
状態を系統的に調べることであり，アルゴリズムや技法によっ
ていくつかのツールが開発された．SPIN モデル検査器 [9] は，
モデル検査ツールの中に，一番実用的だと考えられ，実践的な
報告もいくつかあった [17].
takefromS : set of myNat ==> set of myNat
takefromS(a) == ( pool := pool \ a; return pool )
pre card a <= 2 and card a > 0
post card pool <= card pool~;
end SIMPLE
図 1 簡単な VDM-SL 記述：モジュール SIMPLE
込み C 機能を使って，VDM インタプリタの VDMJ [10] を統
SPIN は，PROMELA といったモデリング言語でシステム
と性質を記述した検証モデルから C 言語の検査器 pan.c を生
成して検査を行う．いくつかの設定が設けられていて検査時の
マシンのリソースに応じて検査のプロセスをチューニングする
ことできる．
合する．この統合により，VDM モデルを実行する PROMELA
SPIN では組み込み C(embedded C code) [18] といった特別
モデルを構築する．この手法は，VDM モデルを検証モデル
な機能がある．この機能を用いて C 言語のソースコードと組
に変換する手法とは違い，VDM の意味論をそのまま保持す
み合わせたハイブリットな検証モデルを構築する．このハイブ
ることであるが，その代わりに，実装に関する手間が増える．
リット検証モデルにおいて，PROMELA はソフトウェアに対
また，VDM の意味論をそのまま使うため，従来の VDM-SL
する環境やユーザの振る舞いを表現し，組み込み C は実際の
と VDM++だけではなく、リアルタイム仕様記述を支援する
ソフトウェアの C コードを実行させる．本稿で提案する手法
VDM-RT まで拡張可能な利点がある．
は，SPIN の組み込み C 機能を利用して VDM インタプリタの
2. 予 備 知 識
本章では，VDM と SPIN について紹介する．
2. 1 VDM
VDM (Vienna Development Method) は，初めて 1970 年代
VDMJ と組み合わせたハイブリットモデルを構築することで
ある．
3. SPIN を用いた VDM 仕様に対するモデル
検査手法
に IBM のウイーン研究所で開発された [11]．VDM の仕様記述
本章は，ハイブリット検証モデルといった基本アイデアから
言語（VDM-SL）は高階記述言語で形式的な文法と意味論が定
オートマトン定義，そして実装方式に関して提案手法を説明
義されている [12], [13]．
する．
VDM にはいくつかの抽象型を提供している：ブーリアン
(bool)，自然数 (nat)，トークン (token) などからなる基本型，
3. 1 ハイブリット検証モデル
図 2 は提案手法のハイブリット検証モデルのアイデアを示す
及びレコード (record)，直積 (product)，集合 (set)．写像 (map)
状態遷移機械の断片である．図 2 で示すように，我々が考え
などからなる複合型がある．VDM モデルの中には，変数（ま
ているのはステートチャートのような大域状態変数及び VDM
たは状態変数）が不変条件で制約され，関数・操作が事前・事
モデルが含まれている状態遷移機械である．このような状態
後条件で制約される．例えば，図 1 では SIMPLE モジュールと
遷移機械の状態は，状態遷移機械の状態，大域変数の値，及び
いった簡単な VDM-SL モデルをが示す．このモジュールでは
VDM モデルの状態で構成される．状態遷移は UML 状態図の
状態変数 pool を 0..9 が要素となる集合に定義した．状態変
ように [condition]/action で構成される．condition がガード
数に 0..9 の自然数を入れたり取ったりする操作，putintoS と
条件で action がアクションやイベントの実行である．直接な
takefromS が定義された．制約条件として myNat といった型の
定義ではないが，状態の中の entry/exit アクションを表現する
不変条件，及び二つの操作の事前・事後条件が定義された．
ことも可能である．また，状態遷移のアクション実行において，
VDM モデルの関数と操作を利用する場合は関連の大域変数及
VDM モデルを構築するための GUI ツールが主に二つあ
び VDM モデルの変数に値の更新が発生する．
る：Overture Tool [14] と VDMTools [15]．これらのツールは，
VDM モデルの正当性確認と検証のための文法と型の検査及
3. 2 ハイブリット検証モデルの拡張オートマトン定義
び仕様アニメーション（インタプリタ [12] による実行）をサ
前節では提案手法のアイデアのハイブリット検証モデルを
ポートしている．VDM の仕様記述言語は，VDM-SL 以外にも
UML の状態図に類比するが，定義を与えるときは必ずしも
VDM++ [2] と VDM-RT [16] がある．VDM++は VDM-SL の
UML の状態図に限られていない．本節では拡張オートマトン
—2—
Hybrid Model
EAV DM は，変数及び VDM モデル付きの有限状態オート
Global variable definitions,
VDM models (types, functions, operations, constraints)
マトンで定義され，図 2 で示されたハイブリット検証モデルを
表現する．一つの状態遷移において，ガード条件はブーリアン
[cond.] / action
図2
式で表現し，アクションは算術演算式のシーケンスで表現する．
どの式においても VDM モデルで定義された関数や操作を利用
ハイブリット検証モデル
でハイブリット検証モデルを定義する．まずは VDM モデルに
ついて定義する．
（VDM モデル） VDM モ デ ル は タ プ ル M
［定義 1］
する場合がある．アクションが実行された結果として大域変数
及び VDM モデルの状態変数の更新が伴うことである．
また，ガード条件式やアクション式の中において，一般的な
=
(T ypes, V ar, V alues, Inv, F un, Ope) で表現する,
式以外に，VDM モデルの関数や操作を利用する式がある．こ
の場合，VDM モデルの定義に基づく評価が必要になり，一般
- T ypes：型の集合．
的な評価方式では評価できない．提案手法では，この問題に対
- V ar：
（状態）変数の集合．
して，VDM インタプリタを用いた VDM 評価関数を定義 3 で
- type(v) ∈ T ypes：変数 v ∈ V ar の型.
- V alues：定数の集合．
- type(v ) ∈ T ypes：定数 v ∈ V alues の型.
用意する．これらの VDM 評価関数は，評価したい VDM モデ
ルの関数や操作，及び関連する入力と出力の変数と合わせた式
を評価する．
- Inv = {inv t | t ∈ T ypes} ∪ {inv V ar}：不変条件の集合． ［定義 3］（VDM 評価関数） VDM モ デ ル M = (T ypesM ,
- F un：関数の集合．
- in f と out f ：関数 f ∈ F un の入出力のシグネチャ．
- pre f と post f ：関数 f ∈ F un の事前条件と事後条件．
- Ope：操作の集合．
- in op と out op：操作 op ∈ Ope の入出力のシグネチャ．
- pre op と post op：操作 op ∈ Ope の事前条件と事後条件．
V arM , F unM , OpeM ) において，変数の集合 V ，V arM ⊂
=V
が与えられた場合に VDM の関数や操作に対する評価関数を定
義する：
- evalV DM = 2V × F unM ∪ OpeM × 2V → () | Error
- boolevalV DM = 2V × F unM ∪ OpeM → Bool | Error
定義 3 では，二つの VDM 評価関数を定義した．一つは VDM
定義 1 で示されたのは，VDM モデルに types，values，vari-
の関数・操作と型を用いた算術演算のための評価関数で，もう
ables，invariants，functions，と operations の定義ブロックが
一つは VDM の関数・操作と型を用いたブーリング演算のため
ある．この定義の目的は，提案手法での検証に必要な VDM モ
の評価関数である．ブーリング演算の場合，出力が必要なく，
デルの情報を提供することであり，実際の定義ブロックの詳細
ブール値を返すだけになる．また，VDM の操作を用いて評価
は VDM-SL と VDM++の文法で記述されている．ハイブリッ
する場合，VDM の意味論に従って，出力変数のほかに VDM
ト検証モデルには，VDM モデルを定義 1 のような定義ブロッ
モデルの状態変数も更新される．更に，どの VDM 評価関数も
クが含まれている．実際の VDM モデルは，複数のモジュール
VDM モデルで定義した制約条件（事前・事後条件と不変条件）
やクラスを定義するのが普通だが，検証の目的には，合わせた
に違反があった場合，Error を返り値として返す．
一つのモジュールやクラスで考えることが十分である．これら
の VDM の定義ブロックをもって，次にハイブリット検証モデ
ルを表現する拡張オートマトンモデル EAV DM を定義する．
（EAV DM ） VDM モデル M = (T ypesM , V arM ,
［定義 2］
V aluesM , InvM , F unM , OpeM ) に 基 づ く ハ イ ブ リット 検
証モデルは，拡張オートマトン EAV DM で表現する：P =
(S, s0 , V, E, T , A, F ),
- S ：状態の集合．
3. 3 ハイブリット検証モデルの構築
本節では，定義 2 で定義した EAV DM （ハイブリット検証モ
デル）の構築方法について述べる．提案手法では，ハイブリッ
ト検証モデルを図 3 で示した構造で構築する．モデルの主な
構造として PROMELA モデルの記述がある．PROMELA モ
デルは，ソフトウェアに対する環境またはユーザの振る舞いを
記述する．例えば，図 1 のモジュールに対して，初期状態から
putinsoS と takefromS を非決定的に起させる環境であれば全
ての状況が表現できる．
- s0 ∈ S ：初期状態．
- V = VM ∪ VL ：
（状態）変数の集合；VL ：ローカル変数．
- ρ：型のシグネチャから（状態）変数の集合への写像．
- E = G × Θ：イベント・アクションの集合．
- G ：ガード条件の集合．
- Θ：
（状態）変数を更新する関数の集合．
- A：述語の集合．
- T⊂
=S × E × S ：状態遷移の集合．
- F⊂
=S ：終了状態の集合．
PROMELA モデルの中に，VDM モデルの定義に基づく評
価について，定義 3 の評価関数の実装が必要になる．提案手法
では SPIN の組み込み C と VDMJ を組合せて実装する．具体
的には，VDM モデルの定義において，それぞれの関数と操作
に対応した C 関数を実装する．SIMPLE モジュールの場合，二
つの操作とそれらの事前条件に対して，４つの C 関数を実装す
る．事前条件に対する評価関数は，状態遷移のガード条件式に
使う．
C 関数の内容は，VDMJ を通して VDM モデルの関数や操
—3—
Hybrid Model
PROMELA
Model
Embedded C
C code
(types)
Var. decl.
C code
(func./op.)
Evaluate
VDM expr.
VDM Model
(VDM-SL/VDM++)
load/evaluate
Constraints
VDMJ
(interpreter)
Property
(Never Claim)
図 3 ハイブリット検証モデルの構造
作を実行させて返り値を受け取ることを行うコードである．具
体的に，VDMJ は Java で実装されたため，Java プロセスと
C プロセス (pan.c) の間には pipe を利用した通信で評価関数
を実現する．また，今の実装方式では，PROMELA で定義し
た状態変数だけが検査アルゴリズムに検査されるため，VDM
モデルの状態変数に対応する変数も定義する必要がある．従っ
て，PROMELA モデルと VDM モデル間において状態変数の
同期が必要になる．
PROMELA モデルでは，VDM モデルで定義した型の変数
を扱うことがあるため，対応する型の宣言を記述しなければな
らない．しかし，VDM の集合や写像といった型に直接に対応
する C/RPROMELA の記述方法がない．この問題について，
提案手法では，これらの複合型に対して，C/PROMELA で配
列と長さを表す整数で構成された構造体で記述する．実際に事
例で使ってみた上，このような構造体による記述は，多くの場
合の VDM の型に対応できると分かった．整数や自然数以外の
基本型に対しては，mtype または enum で対応する．もう一つ
の問題は，型の制約を反映することである．現在は，型の不変
条件に対して，直接に条件式で C/PROMELA の上で表現でき
ないため，気を付けて制約を適切に値を指定するときに反映す
ることが現状である．
4. 事
例
4. 1 モジュール SIMPLE
我々は提案手法をもって図 1 の簡単なモジュール SIMPLE に
適用してみた．このモジュールを検証する目的として，12 行目
で記述されている不変条件の違反が可能かどうかである．この
不変条件は，pool といった VDM モデルの状態変数が 2 と 8
だけの集合になってはいけないと記述された．この不変条件の
検証は，状態変数の 210 = 1, 024 の状態空間の中に一つの状態
を特定することと同じである．
前節でも述べたように，この事例は直観的な環境：初期状態
から非決定的に putintoS と takefromS を起こす振る舞いで
PROMELA モデルを記述した．
1
2
3
4
5
c_decl{\#include "simple_types.c"}
c_code{\#include "simple_ops.c"}
// state of SIMPLE module
typedef SIMPLE_S {
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
byte length = 0; // size
byte pool[10]; // pool : set of myNat
(0~9)
}
// set of nat (input of operations in SIMPLE module)
typedef set_myNat {
byte length = 0;
byte numbers[2]; // max length: 2
}
SIMPLE_S state_simple;
set_myNat param;
bool VDM_Error = 0;
active proctype simple() {
c_code{ initialization(); read_state_SIMPLE(); };
do
:: sel_set_mynat_param(param);
if
:: c_expr{ pre_SIMPLE_putintoS()? } ->
c_code{ write_state_SIMPLE(); }
c_code{ SIMPLE_putintoS(); }
c_code{ read_state_SIMPLE(); };
:: c_expr{ pre_SIMPLE_takefromS() } ->
c_code{ write_state_SIMPLE(); }
c_code{ SIMPLE_takefromS(); }
c_code{ read_state_SIMPLE(); };
fi;
:: break
od;
}
上記の PROMELA コードは，関連する部分の RPOMELA
モデルを示した（注 1）．まずは二つの C ファイルをインクルード
した (行 1-2)．一つ目のファイルは変数の型（VDM 型を含む）
及び補助型や変数の定義で，もう一つのファイルは関数や操作
の C 関数の実装である．行 4-14 では，SIMPLE の型の S と set
of myNat の構造体を用いた宣言である．これらの構造体は，前
述のように，byte の配列と長さ length から構成される．
行 21-35 では，状態遷移の記述である．一つの状態遷移は，
ガード条件とアクション実行以外に，PROMELA と VDM モ
デルの状態変数の同期も必要である．例えば，行 26-28 までは，
putintoS の評価の read state SIMPLE() の前後にも状態変
数 state simple を同期するためのアクションが記述された．
この例題の検証用の性質は，!<> VDM error == 1 にした．
行 18 ではこの性質のための特殊な変数 VDM error を定義した．
VDM error は SIMPLE が制約条件に違反する合図として，評価
用関数 SIMPLE putintoS() と SIMPLE takefromS() が VDMJ
からランタイムエラーを受けたときに１にセットされる．
never {
/* <> (VDM_Error==1) */
skip
T0_init:
do
:: atomic { ((VDM_Error==1)) -> assert(!((VDM_Error==1))) }
:: (1) -> goto T0_init
od;
accept_all:
skip
}
この検証モデルに対して実際に SPIN でモデル検査を行った
結果は以下の通りである．
pan:1: assertion violated !(VDM_Error==1) (at depth 406680)
pan: wrote simple.pml.trail
...
State-vector 32 byte, depth reached 406687, errors: 1
（注 1）：入力を列挙するためのインライン関数 sel mynat param に関する記述は
省略した．この関数は myNat で構成されるサイズが１か２の集合を列挙する
—4—
545237 states, stored
52645 states, matched
597882 transitions (= stored+matched)
0 atomic steps
hash factor: 246.164 (best if > 100.)
bits set per state: 3 (-k3)
Stats on memory usage (in Megabytes):
18.719 equivalent memory usage for states
16.000 memory used for hash array (-w27)
16.000 memory used for bit stack
38.147 memory used for DFS stack (-m1000000)
70.733 total actual memory usage
pan: elapsed time 33.5 seconds
pan: rate 16266.02 states/second
検査結果として，検査機が不変状態違反を見つけて反例報告
をした．モデル検査の実行環境は，Intel Core i5 2.3GHz CPU
と 4GB RAM である．探索深さの設定は 1,000,000 である．不
変状態違反の時に VDMJ が返した報告は以下の通りである．
ERROR returned by VDMJ interpreter...
read:
Error 4131: State invariant violated:
inv_S in ’SIMPLE’ (simple.vdmsl) at line 22:21
Stopped in ’SIMPLE’ (simple.vdmsl) at line 22:21
22:
takefromS(a) == ( pool := pool \ a; return pool )
4. 2 議
論
本節では，モジュール SIMPLE に提案手法の適用結果から提
案手法について議論する．
使いやすさ： 現状では，ハイブリット検証モデルの構築ため
に，手作業で PROMELA 及び関連の C コード記述を完成しな
ければならない．この部分から見ると，提案手法のコストがま
だ高いと考えられる．ただし，事例に適用した成果物として，
組み込み C のコードブロックや関数をいくつかできた．これら
の成果物は他の事例に再利用またはテンプレートとして利用で
きる．例えば，VDMJ と pipe 経由でやり取りするコードはそ
のまま再利用できる．VDM 評価関数の実装でできた C 関数は，
簡単な修正で他の事例で利用できる．また，VDM モデルの状
態変数と PROMELA の状態変数と同期するための VDMJ の
返り値を解析するパーサー付き C コードも再利用できる．現状
では，VDM の型に対応する C/PROMELA 記述はまだ系統的
ではないが，構造体のスタイルは形として再利用できる．
スケーラビリティ: SIMPLE 事例では，大規模ではないが，入
力変数の列挙の過程で状態数が増えてしまう現象があった．この
問題に対して，一つの対策は，VDM モデルを検証目的の抽象化
を行う．もう一つの対策は，Swarm Verification Technique と
いった SPIN の大規模システムに適用する戦略を導入する [19]．
また，VDM の型，特に集合や写像などの複合型を列挙する
場合，C/PROMELA の記述より，制約論理プログラミング
（Constraint Logic Programming, CLP） [20] のほうが対応し
やすい．従って，CLP を PROMELA モデルに導入することも
考えられる．
実行効率： モジュール SIMPLE の適用事例から見ると，実行
効率は状態空間に比べて遅いほうである．その理由は，提案
手法の実装では C プロセスのほかに，VDMJ といった独立の
Java プロセスを立ち上げることにある．従って，検証のプロセ
スは，実際に二つのプロセスを実行させることで，プロセス間
の pipe 通信によって I/O のロードが大きくなり，実行効率が
下げられてしまう．この問題に対して，今後の方向として，独
立したプロセスではなく，VDMTools の C++の API を利用
することで解決できると考える．
5. 関 連 研 究
VDM モデルに対するモデル検査を適用する研究はいくつ
かある．K. Lausdahl [21] は，意味論を保持するモデル変換手
法を提案した．この変換手法は，VDM-SL の意味論の一部を
Alloy モデルに変換し，Alloy でモデル検査を行うことである．
この手法の目的は，陰仕様の VDM-SL モデルの事前事後条件
及び不変条件の整合性確認である．実際には，VDM-SL 陰仕
様モデルの制約条件（関数や操作の事前・事後条件，及び状態
変数や型の不変条件）を Alloy モデルに変換し，指定された実
行系列をもって VDM モデルの制約条件に合うようなインスタ
ンスが存在するかを確認する．
また，K. Lausdahl ら [22] は，上記モデル変換手法の代わ
りに，ProB [23] に変換する手法を提案した．この手法の目的
は，陰仕様で記述した VDM モデル（VDM-SL か VDM++）
にあった関数または操作に対して，陽仕様のためのボディの記
述を生成することでなる．具体的なやり方は，陰仕様として
記述された VDM モデルにあった関数や操作に対して，事前・
事後条件，不変条件，及び規定された入力を ProB に変換し，
ProB の制約ソルバーの機能を利用して解を求める．そして，
ProB で求めた解は，VDM モデルの陽仕様のボディに変換し
て VDM の陽仕様記述を完成する．
上記二つの手法の共通点として，VDM モデルの陰仕様記述
に対するモデル変換を行うところにある．モデル変換手法は，
理論的に対応をとりやすいが，VDM の型や式の表現が他の形
式記述より豊富なため，変換しにくいところが多い．従って，
陰仕様記述を対象にしては変換範囲を小さくする効果もある．
これらモデル変換を行う手法に対して，提案手法ではモデル検
査のためのハイブリット検証モデルを構築する．従って，VDM
モデルを検証モデルに変換することがなく，VDM の意味論を
そのまま扱うことができる．また，提案手法は，陰仕様ではな
く陽仕様で記述された VDM モデルを対象にするため，主な
VDM モデルの検証・確認手段のインタプリタによる実行（仕
様アニメーション）を活用することとなる．更に，提案手法で
は，スレッドとスケジューリングの対応ができれば，リアルタ
イムシステム向けの VDM-RT に適用することが可能だと考え
られる．
一方，提案手法でのハイブリット検証モデルの構築テクニック
は，VDM インタプリタのソースコードへの拡張や連携とも考え
られる．B. Frohlich と P. G. Larsen [24] は VDM-SL Toolbox
と C++コードの連携手法を提案した．この手法は VDM-SL の
インタプリタの意味論を拡張して関数や操作の実行が外部 C++
コードの実行で行うことが可能にする．これは提案手法の VDM
評価関数（定義 3）の逆方向となる．C. B. Nielsen ら [25] は，
VDMJ の ECI(external call interface) と RCI(remote control
interface) を利用して VDM モデルと Java コードの連携を実
現した．この手法は主に VDM モデルのアニメーションするた
めの GUI の構築に使う．この手法のように直接インタプリタ
—5—
の API を通して VDM モデルを実行することは，我々の提案
手法にとっては検証効率改善の方向性を示すことでもある．
6. 終 わ り に
本稿では，VDM 仕様モデルに対して SPIN を用いたモデル
検査手法を提案した．モデル検査を行うために，我々は VDM
モデルに基づいてハイブリット検証モデルを構築する．ハイブ
リット検証モデルの構築には，SPIN の組み込み C 機能を用
いて PROMELA モデルと VDM インタプリタの VDMJ を組
み合わせる．この手法によって，VDM モデルに対して論理モ
デル検査の適用が可能になる．提案手法は現在，VDM-SL と
VDM++に適用できるが，スレッドのスケジューリングを対応
できれば VDM-RT までの対応が可能である．
簡単な例題ではあるが，本稿では提案手法の適用実験を行っ
た報告を述べた．適用事例の結果をもって我々は使いやすさ，
スケーラビリティ，及び実行効率について議論した．使いやす
さについて，現在のハイブリット検証モデルの構築には手作業
が多くてコストがかかる．対策として，事例で記述した C コー
ドの再利用性を高める以外に，系統的な対応法も必要である．
スケーラビリティの対応について，検証目的の VDM モデルの
抽象化，及び SPIN の大規模システムへの対応テクニックの導
入が考えられる．実行効率を上げるために，独立した VDMJ
の Java プロセスの代わりに，VDMTools の C++ API を利用
して VDM 評価関数を実装する方向性が考えられる．
謝
辞
本研究は JSPS 科研費基盤研究 (S)24220001 の助成を受けた
ものです。
文
献
[1] C. B. Jones, Systematic Software Development Using VDM,
2nd Ed. Upper Saddle River, NJ, USA: Prentice-Hall, Inc.,
1990.
[2] J. Fitzgerald, P. G. Larsen, P. Mukherjee, N. Plat, and
M. Verhoef, Validated Designs for Object-oriented Systems.
Santa Clara, CA, USA: Springer-Verlag TELOS, 2005.
[3] J. Fitzgerald and P. G. Larsen, Modelling Systems: Practical Tools and Techniques in Software Development, 2nd
Edition. Cambridge University Press, 2009.
[4] P. G. Larsen and J. Fitzgerald, “Recent industrial applications of VDM in Japan,” in Proceedings of the 2007th
Internatioanal Conference on Formal Methods in Industry,
ser. FACS-FMI’07. Swinton, UK, UK: British Computer
Society, 2007, pp. 8–8.
[5] T. Kurita, M. Chiba, and Y. Nakatsugawa, “Application of
a formal specification language in the development of the
“Mobile FeliCa” IC chip firmware for embedding in mobile
phone,” in FM 2008: Formal Methods, 15th International
Symposium on Formal Methods, 2008, pp. 425–429.
[6] T. Kurita and Y. Nakatsugawa, “The application of VDM
to the industrial development of firmware for a smart card
IC chip,” Int. J. Software and Informatics, vol. 3, no. 2-3,
pp. 343–355, 2009.
[7] Y. Nakatsugawa, T. Kurita, and K. Araki, “A framework
for formal specification considering review and specificationbased testing,” in TENCON 2010 - 2010 IEEE Region 10
Conference, Nov 2010, pp. 2444–2448.
[8] E. M. Clarke Jr., O. Grumberg, and D. A. Peled, Model
Checking. The MIT Press, 1999.
[9] G. Holzmann, Spin model checker, the: primer and reference manual. Addison-Wesley Professional, 2003.
[10] “VDMJ.” http://sourceforge.net/projects/vdmj/
[11] D. Bjørner and C. B. Jones, Eds., The Vienna Development Method: The Meta-Language, ser. Lecture Notes in
Computer Science, vol. 61. Springer, 1978.
[12] P. Larsen and P. Lassen, “An executable subset of Meta-IV
with loose specification,” in VDM’91 Formal Software
Development Methods, ser. Lecture Notes in Computer
Science, S. Prehn and W. Toetenel, Eds. Springer Berlin
Heidelberg, 1991, vol. 551, pp. 604–618.
[13] P. G. Larsen and W. Pawlowski, “The formal semantics
of ISO VDM-SL,” Computer Standards & Interfaces,
vol. 17, no. 5?6, pp. 585 – 601, 1995, formal Description
Techniques.
[14] P. G. Larsen, N. Battle, M. Ferreira, J. Fitzgerald,
K. Lausdahl, and M. Verhoef, “The Overture initiative
integrating tools for VDM,” SIGSOFT Softw. Eng. Notes,
vol. 35, no. 1, pp. 1–6, jan 2010.
[15] J. Fitzgerald, P. G. Larsen, and S. Sahara, “VDMTools:
Advances in support for formal modeling in VDM,”
SIGPLAN Notices, vol. 43, no. 2, pp. 3–11, feb 2008.
[16] M. Verhoef, P. Larsen, and J. Hooman, “Modeling and
validating distributed embedded real-time systems with
VDM++,” in FM 2006: Formal Methods, ser. Lecture
Notes in Computer Science, J. Misra, T. Nipkow, and
E. Sekerinski, Eds. Springer Berlin Heidelberg, 2006, vol.
4085, pp. 147–162.
[17] G. J. Holzmann, “Mars code,” Commun. ACM, vol. 57,
no. 2, pp. 64–73, feb 2014.
[18] G. Holzmann and R. Joshi, “Model-driven software verification,” in Model Checking Software, ser. Lecture Notes in
Computer Science, S. Graf and L. Mounier, Eds. Springer
Berlin Heidelberg, 2004, vol. 2989, pp. 76–91.
[19] G. J. Holzmann, R. Joshi, and A. Groce, “Swarm
verification techniques,” IEEE Trans. Softw. Eng., vol. 37,
no. 6, pp. 845–857, nov 2011.
[20] M. Triska, “The finite domain constraint solver of SWIProlog,” in FLOPS, ser. LNCS, vol. 7294, 2012, pp. 307–
316.
[21] K. Lausdahl, “Translating VDM to Alloy,” in Integrated
Formal Methods, ser. Lecture Notes in Computer Science,
E. Johnsen and L. Petre, Eds. Springer Berlin Heidelberg,
2013, vol. 7940, pp. 46–60.
[22] K. Lausdahl, H. Ishikawa, and P. G. Larsen, “Interpreting
Implicit VDM Specifications using ProB,” in Proceedings
of the 12th Overture Workshop, Newcastle University, 21
June, 2014, N. Battle and J. Fitzgerald, Eds. School of
Computing Science, Newcastle University, UK, Technical
Report CS-TR-1446, January 2015.
[23] M. Leuschel and M. Butler, “ProB: a model checker for
B,” in FME 2003: Formal Methods, ser. Lecture Notes in
Computer Science, K. Araki, S. Gnesi, and D. Mandrioli,
Eds. Springer Berlin Heidelberg, 2003, vol. 2805, pp.
855–874.
[24] B. Fröhlich and P. Larsen, “Combining VDM-SL specifications with C++ code,” in FME’96: Industrial Benefit
and Advances in Formal Methods, ser. Lecture Notes in
Computer Science, M.-C. Gaudel and J. Woodcock, Eds.
Springer Berlin Heidelberg, 1996, vol. 1051, pp. 179–194.
[25] C. Nielsen, K. Lausdahl, and P. Larsen, “Combining
VDM with executable code,” in Abstract State Machines,
Alloy, B, VDM, and Z, ser. Lecture Notes in Computer
Science, J. Derrick, J. Fitzgerald, S. Gnesi, S. Khurshid,
M. Leuschel, S. Reeves, and E. Riccobene, Eds. Springer
Berlin Heidelberg, 2012, vol. 7316, pp. 266–279.
—6—