早稲田大学大学院基幹理工学研究科情報理工学専攻

(1)

2010 年度修士論文

インタラクティブなモデルの検査を可能にする LMNtal ビジュアルツールの設計と実装

提出日： 2011 年 1 月 27 日指導：上田和紀教授

早稲田大学大学院基幹理工学研究科情報理工学専攻

学籍番号： 5109B003-7

綾野貴之

(2)

概要

情報システムに大きく依存している現代社会において，ソフトウェアの障害や誤作動は大きな損失をもたらし，人命にも関わる重大な事故を起こす危険性をはらんでいる．そのような背景からソフトウェアの品質を向上させるための手段としてモデル検査技術が注目を集めている．モデル検査とはモデル記述言語を用いてシステムの動作を有限状態遷移系にモデル化し探索する検証手法であり，網羅的探索によってモデルの不具合を発見する．

階層グラフ多重集合書き換えに基づく状態遷移系記述言語LMNtalにおいても2007年よ

りLMNtalをモデル記述言語とするモデル検査器の構築が行われ，高信頼なシステム構

築をサポートするようになった．LMNtalモデル検査器は検査のための特別な準備を最低限にするよう設計されており，LMNtalで記述されたほどんどすべてのシステムを対象に仕様を満たすか判定することができる．同一の言語で開発と検証を可能にすることで，探索や検証分野にも拡大し広範な応用を目指している．

本研究でもモデル検査の応用を開拓すべく，新たに検証をビジュアライズする環境の構築を行った．LMNtalモデル検査器やコンパイラ，プログラム実行可視化ツールなどの各

種LMNtal処理系をユーザーが容易に操作できるように統合開発環境LaViTの設計と実

装を行い，その統合された環境の1つの機能として検証ビジュアルツールStateViewer を提供した．

StateViewerはLMNtalモデル検査器からの情報を解析してモデルの全状態遷移グラ

フや検証結果の可視化を行う．しかし探索深度を揃えた状態描画などをするものの，モデルの性質によって状態遷移グラフの形状も大きく異なるため単一の描画方法では対応しきれなかった．そこでどのような状態遷移グラフでも可能な限りわかり易く正確に把握できるようにするため，状態と遷移が重ならないようにするダミーノードの導入や3D空間での描画，遷移関係の解析による状態配置，遷移をバネに見立てた力学による状態配置などの工夫を行った．また単にグラフの描画を行うだけではなく，実行シミュレーション機能や状態検索機能，遷移検索機能などシステムの性質を解析するための機能をGUIで提供した．特にLMNtalの性質に着目し，同一書き換え規則で状態遷移可能な状態集合を1 つの状態に抽象化を行うことで，組み合わせ爆発を起こした状態空間をブラウジング可能なサイズにまで状態数削減を行う状態集合抽象化機能も実装した．

ユーザーはこれらの機能を適宜使用することでインタラクティブなモデルの検査ができ，システムの理解を深めることが可能となっている．書き換え規則の不備や仕様外のデッドロックの発生検出，対称性の発見などテキストだけでは見逃す可能性の高い重要なモデルの性質をユーザーに提供できるようになった．

(3)

図目次

1.1 ユーザーインターフェースjSpinの実行例 . . . 3

1.2 SpinSpiderによってGraphvizが生成した状態遷移グラフの画像 . . . . 3

1.3 モデル検査器LTSAの実行例 . . . 4

2.1 LMNtal構成要素 . . . 7

2.2 LMNtalの構文規則 . . . 8

2.3 プロセスの型の範囲 . . . 10

2.4 LMNtalの比較演算子 . . . 10

2.5 UNYO UNYOの実行画面 . . . 13

3.1 LMNtalにおけるLTLモデル検査の流れ . . . 16

4.1 LaViTの開発支援機能. . . 21

4.2 LaViTと他処理系の構成 . . . 22

4.3 検証支援機能のインターフェース . . . 24

4.4 有限状態モデルに対するStateProﬁlerの実行. . . 25

4.5 無限状態モデルに対するStateProﬁlerの実行. . . 25

5.1 LaViTが使用する他処理系の構造 . . . 27

5.2 LaViTのインターフェース構造 . . . 28

6.1 StateViewer実行例の全体図 . . . 31

6.2 初期配置(Church数2の2乗) . . . 37

6.3 Adjust Resetよる配置(Church数2の2乗) . . . 37

6.4 力学モデルによる配置(Church数2の2乗) . . . 37

6.5 抽象化機能の適用(Church数2の2乗) . . . 37

v

(7)

6.6 初期配置(ハノイの塔) . . . 38

6.7 Adjust Resetよる配置(ハノイの塔) . . . 38

6.8 力学モデルによる配置(ハノイの塔) . . . 38

6.9 初期配置(水差しの問題) . . . 39

6.10 Adjust Resetよる配置(水差しの問題) . . . 39

6.11 力学モデルによる配置(水差しの問題) . . . 39

6.12 Adjust Reset配置後ダミー導入(水差しの問題) . . . 39

6.13 Dummy Mix Adjustよる配置(水差しの問題) . . . 39

6.14 垂直方向の遷移の重なり . . . 40

6.15 Set Vertical Dummyの適用. . . 40

6.16 3D StateViewerの実行例 . . . 40

6.17 実行シミュレーション機能の実行例 . . . 41

6.18 LMNtalルール構文を用いた状態検索の実行例 . . . 42

6.19 ルール名による遷移検索の実行例 . . . 42

6.20 検索をした3D StateViewerの実行例 . . . 42

6.21 通常のState Viewerによる実行. . . 43

6.22 3D State Viewerによる規則性の発見 . . . 43

6.23 LTL StateViewerの実行例 . . . 44

6.24 LTL StateViewerの3D実行例 . . . 44

7.1 モデル検査器SLIMとStateViewerの処理の流れ . . . 51

7.2 ダミーノードを制御点とするベジエ曲線の描画 . . . 52

7.3 簡単なプログラムへのAdjust Reset機能適用例 . . . 52

7.4 重なった状態の間隔を均等にあける . . . 53

7.5 重なった状態の間隔を再帰的に均等にあける . . . 53

7.6 抽象化機能の実装の概要 . . . 54

8.1 Petersonのアルゴリズムの状態遷移グラフ . . . 56

8.2 Petersonのアルゴリズムを検証するための記述. . . 57

8.3 Petersonのアルゴリズムのエラーサイクルの描画 . . . 58

8.4 エラーサイクルが検出されないLTL StateViewerの実行 . . . 58

8.5 エレベーターモデルにおけるStateViewerの実行 . . . 60

8.6 エレベーターモデルにおける3D StateViewerの実行 . . . 60

vi

(8)

8.7 エレベーターモデルにおけるエラーサイクルの検出 . . . 61 8.8 エレベーターモデルにおけるエラーサイクルの検出(3D) . . . 61 8.9 53万状態の描画 . . . 62

vii

(9)

表目次

4.1 処理系操作ボタンの説明 . . . 23

5.1 LMNtal処理系の実装言語 . . . 29

6.1 Control Buttonタブの機能一覧(1) . . . 45

6.2 Control Buttonタブの機能一覧(2) . . . 46

6.3 Otherタブの機能一覧 . . . 47

6.4 右クリック時の機能一覧 . . . 48

6.5 マウスとキーボードの操作一覧 . . . 49

viii

(10)

1

第 1 _章

はじめに

1.1 研究の背景と目的

LMNtal(Linked Multisets of Nodes transformation language)[1, 2, 18]は階層グラフ多重集合書き換えに基づく状態遷移系記述言語である．階層グラフをルールと呼ばれる書き換え規則によって動的に変化させることで，複雑なデータ構造を操作するプログラムや多重集合書き換えを伴うプログラムを簡潔に記述することができる豊富な表現力を有する．

そこで LMNtalの並行言語の特性と高い表現力を生かし，2007年からLMNtalをモ

デル記述言語としたモデル検査器SLIM(Slim Lmntal IMplementation)[5]を開発している．モデル検査とは，モデル記述言語を用いてシステムの動作を有限状態遷移系にモデル化し，その有限状態遷移グラフを網羅的に探索することによって不具合を発見する自動検証技術である．社会的なシステムの重要性からソフトウェアの信頼性を向上させるための手段としてモデル検査技術が注目を集めている．

LMNtal モデル検査器は，LMNtal実行時処理系で稼動する LMNtalプログラムをほ

とんど修正することなしにそのままモデル検査の対象とすることができる特徴を持ってい

る．このLMNtalモデル検査器は軽量高速化のために JavaによるLMNtal 処理系とは

切り離されてC言語で実装され，現在では最適化が進み並列化[12]などの工夫がなされている．

しかしモデル検査器は定義した仕様に対してエラーが検出されると反例を出力するものの，エラーが検出されない場合はシステムの性質に関する情報は提供されない．また仕様による検査となるため，仕様を超えたシステムの性質は一般的にわからず，予期しないデッドロックや記述者の意図をしない動作などをしている可能性が残る．

(11)

1.2 関連研究 2 これを補うために統合開発環境 LaViT(LMNtal Visual Tools) は，システムの状態遷移グラフを可視化することでモデルの挙動を視覚的に示す検証ビジュアルツール StateViewerを提供している．StateViewerはモデルの全実行経路，さらにはモデル検査の結果の可視化を行い，モデル検査だけでは表現されなかったシステムの性質表現を目的にしている．またユーザーが自ら状態遷移グラフに対して検索機能や抽象化機能をインタラクティブに適用することでさらにシステムの動作の理解を深めることを目的にしている．

またLMNtalにはUNYO UNYO[4, 9]と呼ばれるLMNtalプログラム実行可視化ツールが存在する．このUNYO UNYOはアニメーションでプログラムの処理の進行の表示し動作の把握を容易にすることができる．操作性のためにモデル検査器SLIM同様，Java

によるLMNtal処理系とは独立している．

このように同じ言語で単一のソフトウェアとして実装するのではなく，システムの目的に適した言語選択と設計方法による実装が必要であったためそれぞれ独立して開発された．その結果，LMNtal環境の導入が複雑になってしまい，他処理系を利用するにはそれぞれ異なる実行手順が必要になった．統合開発環境LaViTはモデル検査器 SLIMや実行可視化ツールUNYO UNYOを単一のGUIで導入や起動ができるようにすることも重要な目的として位置付けている．

1.2 関連研究

既存の可視化検証ツールでは，状態数の多い遷移グラフは想定されておらず利用場面は限定されることが多い．またLaViTのStateViewerは状態遷移グラフをインタラクティブに解析する機能を多く提供している点で他の可視化検証ツールと異なる場合が多い．本節では統合開発環境LaViTや検証ビジュアルツールStateViewerの特に重要な関連研究を紹介する．

1.2.1 SPIN のユーザーインターフェース jSpin

Gerard J. Holzmannによって開発されたSPIN(Simple Promela Interpreter)[17] は高速で軽量なモデル検査器である．LMNtal モデル検査器SLIMもSPINのアルゴリズムを一部参考にしている．

SPIN は利用の流れが複雑で高速化やメモリ使用量削減のためのオプションが多く用意されているが，ユーザインターフェースのjSpin[22] を用いて簡略化できる．jSpin の

(12)

1.2 関連研究 3

図1.1 ユーザーインターフェースjSpinの実行例

図1.2 SpinSpiderによってGraphvizが生成した状態遷移グラフの画像

実行例を図1.1に示す．jSpinは主に利便性の向上や導入の簡易化を目的としているが，

LaViTは利便性の向上や導入の簡易化を高めることだけでなく，StateViewerによって

状態遷移グラフを可視化しシステムの性質を表現することを積極的に検証に役立てようとしている点が異なる．

(13)

1.2 関連研究 4

図1.3 モデル検査器LTSAの実行例

jSpin には，モデルの状態遷移の情報をグラフ描画ツールGraphvizに渡し状態遷移グ

ラフを表示するSpinSpiderと呼ばれる機能が存在する．SpinSpiderの実行例を図1.2に示す．描画を汎用的なグラフ描画ツールに任せることで洗練されたグラフ描画を行うことができるが，対象の多い規模の大きな描画にGraphvizは向いておらず，状態遷移グラフは描画対象が多くなりがちなためSpinSpiderは使用範囲が限られている．また画像ファイルとして出力するためインタラクティブな状態遷移グラフの把握には対応していない点がStateViewerと異なる．

1.2.2 モデル検査器 LTSA

LTSA(Labeled Transition System Analyzer)[19]はFSP(Finite State Process)形式の有限状態機械を検証することができる検証統合環境である．LTSAではプロセスの状態遷移を可視化することができ，シミュレーション機能も用意されている．またJavaで実装されており，コンパイルが必要ないため他のモデル検査器と比較して導入や実行が非常に容易である．実行例を図1.3に示す．

ラベル付き遷移系を代数的に表現できるFSPは，データ構造に柔軟性がなく表現力が乏しいためプログラミング言語として一般的に位置付けられていない．しかしLMNtal モデル検査器は階層化が可能で柔軟性に富むデータ構造を持つプログラミング言語LMNtal をモデル記述言語としている．状態遷移グラフを可視化する機能においても，シミュレー

(14)

1.3 本論文の構成 5 ション機能以外にモデルを検査する機能を有しておらず定型化された状態遷移グラフの描画を行うにとどまる．LaViTのStateViewerはシミュレーション機能だけでなく，検索機能や，状態遷移を解析した配置機能，状態遷移に特化して工夫された描画など多くの機能を有する．また LTSAは状態数100の状態遷移のグラフ描画が不可能であるが，

StateViewerは10万状態以上描画できるためスケーラビリティでも優れている．

1.3 本論文の構成

本論文の構成は下記の通りである．

• ^第2章はLMNtalの概要について解説する．

• ^第3章はLMNtalモデル検査について解説する．

• ^第4章はLMNtal統合開発環境LaViTの構成を解説する．

• ^第5章はLMNtal統合開発環境LaViTの設計と実装について解説する．

• ^第6章は検証ビジュアルツールStateViewerの構成を解説する．

• ^第7章は検証ビジュアルツールStateViewerの設計と実装について解説する．

• 第8章は実行画面を用いながらLMNtal統合開発環境の使用例を示す．

• ^第9章は本研究のまとめと今後の課題について述べる．

(15)

6

第 2 _章

LMNtal _言語解説

LMNtal(Linked Multisets of Nodes transformation language)は階層グラフ書き換えに基づく並行言語モデルである．本章では，LMNtalの言語と LMNtalの実行を行うシステムについて説明する．なお本章は文献[1, 2, 18]を基に再構成したものである．

2.1 LMNtal 言語の概要

LMNtalはルールと呼ばれる書き換え規則によって階層グラフを動的に変化させること

で複雑なデータ構造を操作するプログラムや多重集合書き換えを伴うプログラムを簡潔に記述することができる．

2.1.1 LMNtal の構成要素

LMNtalのプログラムはプロセスと呼ばれる4つの要素アトム，リンク，膜，ルールか

ら構成される．

アトムはアトム名と呼ばれる名前と0本以上のリンクを持つ．例えばX,Yの2本のリンクを持つ名前nのアトムはn(X,Y).と記述する．

リンクはアトムを1対1で接続してグラフを構成する．例えばアトムa,bをリンク X で接続したグラフはa(X),b(X).と記述する．

膜はアトムなどの要素の多重集合を構成し，多重集合は入れ子にすることで階層構造を構成する．例えばアトムiをもつ膜は{i}と記述する．さらにこの膜とアトムjをもつ膜は{{i},j}.と記述する．

ルール(書き換え規則) はアトムとリンクと膜からなる階層グラフを動的再構成する．

(16)

2.1 LMNtal言語の概要 7

図2.1 LMNtal構成要素

ルールには名前をつけることができるため，例えばアトムyをアトムzに書き換える名前 rのルールはr@@ y:-z.と記述する．ルール名はプログラム上の動作には影響しないが，

実行時の出力に含まれるようになるためデバッグや挙動の把握に役立てることができる．

LMNtalプログラム

¶ ³

{a(X),b}. c,d(X). d(A):-e(A).

µ ´

を図で表現したものを図2.1に示す．

2.1.2 LMNtal 基本構文

LMNtalの構文規則を図2.2に示す．

P はプロセス，T はルールのプロセス書き換え規則の表現に用いるプロセステンプレートである．0 は中身のないプロセスを表す．p はアトム，X はリンク名を表す．

p(X1, . . . , Xm)はアトムpがm本のリンクを持つことを表す．1つのリンクは2つのアトムを接続する．そのためLMNtalのプロセスは，同じリンク名が2回を超えて出現してはならない(リンク条件)．プロセス P に1回だけ出現するリンク名はP の自由リンクを表す．この自由リンクはプロセスP の外部にあるアトムにつながる．

P, P はプロセスの並列合成， {P} ^は膜 {} によって階層化されたプロセスP である．

ルールT :- T はプロセスの書き換え規則で，膜によって階層化されたプロセスを対象とする．例えば

¶ ³

{ x. { x:-a. }. x:-b. }. x:-c.

µ ´

(17)

P ::= 0 (空)

| p(X1, . . . , Xm) (m≥0) (アトム)

| P, P (分子)

| {P} (セル)

| T:-T (ルール)

T ::= 0 (空)

| p(X1, . . . , Xm) (m≥0) (アトム)

| T, T (分子)

| {T} (セル)

| T:-T (ルール)

| @p (ルール文脈)

| $p[X₁, . . . , X_m|A] (m >0) (プロセス文脈)

| p(*X1, . . . ,*Xm) (m >0) (アトム集団)

A ::= [] (空)

| *X (リンク束)

図2.2 LMNtalの構文規則

では，アトムxと同じ階層にあるルールx :- bだけが適用される．

ルール文脈の@pは膜の中のすべてのルールにマッチする．プロセス文脈の$pは膜の中のルール以外のプロセスのうち，明示的に指定されていないプロセス全体とマッチする．例えば

¶ ³

{ x,$p,@p } :- { $p,@p }.

µ ´

は先の構造において@pは膜内のルールx:-b.にマッチし，$pは膜内の明示されたアトム x以外の構造{x:-a. }.にマッチする．

2.1.3 ガード付きルール

LMNtal のルールには書き換えを行う構造を指定するためにガード付きルールが存在

する．

Head:- Guard|Body

(18)

2.1 LMNtal言語の概要 9 ガードにはプロセスの型や比較演算子が用意されており，プロセスに関する制約を書くことができる．

• int(X)

リンクX の先には1つの整数アトム．

• ﬂoat(X)

リンクX の先には1つの浮動小数点数アトム．

• unary(X)

リンクX の先には1つのアトム．

• ground(X)

リンクX の先には1つ以上接続されたアトム（膜を持たない）．

例えば¶ ³

p(1). p(2.0). p(a). p(a(b,c)). p(a(X)),{b(X)}.

µ ´

を考える．リンクを1 つ持つアトムp が4 つある．アトム p のリンク先にはそれぞれ違ったグラフ構造がある．p(X)としてマッチさせようとしたときにリンクX のガードによってマッチするものが変化する．

• p(X) :- int(X)|. —p(1)にマッチ

• p(X) :- f loat(X)|. — p(2.0)にマッチ

• p(X) :- unary(X)|. — p(1)とp(2.0)とp(a)にマッチ

• p(X) :- ground(X)|. — p(1)とp(2.0)とp(a)とp(a(b,c))にマッチ intとfloatはunaryの部分型であり，unaryはgroundの部分型である．これを図2.3 に示す．

またリンク先のプロセスの型が指定されている場合，そのリンクのリンク条件は満たさなくてよい．例えば

¶ ³

n(p).

n(X) :- a(X),b(X),c(X).

µ ´

はリンク条件を満たしていないためコンパイルエラーとなるが

(19)

図2.3 プロセスの型の範囲

X =Y XとY が等しい (X とY はground型) X\ =Y X とY が等しくない (X とY はground型) X =:=Y X とY が等しい (X とY はint型) X =\ =Y XとY が等しくない (X とY はint型) X < Y X はY より小さい (X とY はint型) X =< Y X はY 以下 (X とY はint型) X > Y X はY より大きい (X とY はint型) X >=Y XはY 以上 (X とY はint型)

図2.4 LMNtalの比較演算子

¶ ³

n(p).

n(X) :- unary(X) | a(X),b(X),c(X).

µ ´

と書くことでアトムpを複製することができるプログラムになる．

またプロセスを比較演算子によって比較することができる．主な比較演算子を図2.4に示す．プロセスに型がある場合のみ比較でき，それぞれの型に対応した比較演算子が用意されている．そのため型指定を省略できる．例えば

(20)

¶ ³

a(3),a(7).

a(X),a(Y) :- X<Y | a(Y).

µ ´

と，整数の比較を行うことができる．

またガード内で新たなint 型のプロセスを定義することができる．これによりガード内で四則演算をすることができる．例えば

¶ ³

a(3),a(7).

a(X),a(Y) :- Z=X+Y | a(Z).

µ ´

を実行すると，新しいアトムa(10)が生成される．

ルール左辺の膜の後に“/”を付加すると，それ以上ルールの適用が起こらない膜にしかマッチしなくなる．これによって子孫膜における計算終了の検出に利用できる．例えば

¶ ³

{

a(3),a(7),a(12).

a(X),a(Y) :- Z=X+Y | a(Z).

}.

{ $p,@p }/ :- $p.

µ ´

は，膜内のルールの適用が終了した後に，膜外のルールがマッチする．

2.1.4 省略構文

LMNtalにはいくつか省略構文がある．

• ^リスト

A_i を第 i要素とするリスト構造をX= [A₁,A₂,. . . , A_n]と書ける．X はリストの先頭につながるリンクである．

• ^項記法

木構造のデータを他言語と同様に記述することができる．アトムaの第k引数として，リンク名の代わりに最終引数を省略したアトムbを書くと，aの第k 引数とb の最終引数とがリンクで接続されているものとみなす．つまりa(b)はa(X),b(X) と等しい．

• ^コネクタ

(21)

2.1 LMNtal言語の概要 12 コネクタと呼ばれる = はリンクの接続を表す．例えば a(X),b(Y),X=Y は， a(X),b(X) と等しい．他の略記法と合わせることで，a(X),b(X) を a=b と略記できる．

• ^{無リンクアトム}

リンクが0本のアトムの括弧()は省略できる．例えばa()は単にaと略記できる．

• ^{前置演算子}

リンクが1本でアトム名が⁰+⁰または⁰−⁰ の場合は前置演算子のように書ける．例えば’+’(X)は+X，’-’(Y)は-Yと略記できる．

2.1.5 コメント

コメントはブロックコメントと一行コメントがある．ブロックコメントは“/*”と“*/”

で囲まれた部分で書くことができる．ただし入れ子にすることはできない．一行コメントは行の“%”か“//”以降がコメントになる．

¶ ³

/*

ブロックコメント

*/

//一行コメント

%一行コメント

µ ´

2.1.6 プログラム例

例として複数の整数の和を求めるLMNtalプログラムを示す．

¶ ³

n(1), n(2), n(3). sum(0).

plus@@ n(N),sum(S) :- M=N+S | sum(M).

µ ´

3つのアトムnと3つの整数アトム1,2,3がリンクでそれぞれ接続されている．またアトムsumと整数アトム0がリンクで接続されている．ルールplusは，アトムnとそれに接続された整数アトム，アトムsumとそれに接続された整数アトムをとり加算したものをアトムsumに接続し直す．このルールを繰り返すことでアトムsumに接続された整数アトムに整数アトムの和を求めることができる．またこのプログラムの解は1 つである

(22)

2.2 LMNtal処理系 13

図2.5 UNYO UNYOの実行画面

が，加算の順序を定めていないため実行過程の非決定性をもつ．

2.2 LMNtal 処理系

Javaによって実装されたLMNtal処理系は大きく分けてコンパイラと実行時処理系からなる．コンパイラは独自に設計した中間命令列へと変換し，それを実行時処理系で解釈実行することができる．他にも中間命令列をそのままテキストとして出力する機能も持っている．また実行時処理系は多言語インターフェースを実装しており，入出力やGUI，ネットワーク接続など機能の拡張を行うことができる．

2.3 LMNtal プログラム実行可視化ツール

LMNtalプログラム実行可視化ツールはLMNtalプログラムの処理の進行を可視化す

ることで実行内容の把握を容易にすることができる．このLMNtalプログラム実行可視化ツールはUNYO UNYO[4, 9]と呼ばれる．実行画面を図2.5に示す．UNYO UNYO は階層グラフを多様な力学アルゴリズムによって動的に再配置を行う．そのためルールの適用やユーザーによる操作によって階層グラフが変化しても柔軟に可視化することができ

る．またLMNtal処理系によるルール適用が行われた差分グラフだけを扱うようにする

など，大規模なグラフを想定した設計と実装がなされている．

(23)

14

第 3 _章

LMNtal _{モデル検査}

LMNtalの処理系はモデル検査機能を有する．本章ではモデル検査の概要と，LMNtal

モデル検査器について述べる．

3.1 モデル検査とは

モデル検査とは，モデル記述言語を用いてシステムの動作を有限状態遷移系にモデル化し，その有限状態遷移グラフを網羅的に探索することによって不具合を発見する自動検証技術である．例えばモデル検査器SPIN[17]ならばPromelaでモデルを記述し状態遷移グラフを網羅的に探索する．仕様の記述は SPINでも採用されている LTL(Linear Temporal Logic)やCTL(Computational Tree Logic)などの時相論理式が用いられ，システムの状態遷移に関する性質を検査することができる．しかし探索する状態空間は組み合わせ爆発を起こしやすく，非常に多くのメモリと時間を必要としてしまう．そのため状態空間の管理手法や状態の圧縮表現手法，状態数削減手法が求められる．

3.2 LMNtal モデル検査器 SLIM

並行言語である LMNtalはルールの実行順序や適用箇所を定めていないため，他の言語よりも容易に非決定性を持たせることができる．また複雑なデータ構造を操作するプログラムや多重集合書き換えを伴うプログラムを簡潔に記述することができる豊富な表現力を有する．そこでLMNtalの並行言語の特性と豊富な表現力を生かし，LMNtal をモデル記述言語としたモデル検査機能[5]を開発している．このLMNtalモデル検査器は SLIM(Slim Lmntal IMplimentation)と呼ばれ，LMNtalで書かれたシステムの信頼性

(24)

3.3 LTLモデル検査の実行方法 15 の向上を図っている．

このモデル検査器SLIMはJavaによる実行時処理系とは別に開発が行われ，動作の高速化とメモリの使用量を抑える設計がされており，実装もC言語で行われている．Java による実行時処理系とはデータの保持の方法が異なるため，1つのアトムのリンク本数は 127本以下，整数アトムなどのデータアトム同士の接続ができないなどいくつかの制約があるが，Javaによる実行時処理系で稼働するほとんどすべてのLMNtalプログラムを SLIMで実行することができる．通常実行でJavaによる処理系と比較すると，10倍以上の高速化と，数分の一にメモリ使用量も抑えることが可能になった．モデル検査機能はこの高速なSLIM実行時処理系に組み込まれる形で実装されたためSLIMで実行できるプログラムをそのままモデル検査の対象にすることができるのが特徴である．

3.3 LTL モデル検査の実行方法

モデル検査器SLIMにおいてLTLモデル検査を行う場合は

• ^{検査対象の}LMNtalプログラムファイル

• 検証したい性質のLTL式を変換したNever Claimファイル

• Never Claim内で使用する命題記号の定義ファイル

の3つのファイルが必要になる．LTLからNever Claimへの変換はLTL2BA[20]を使用する．例えば“常に pが成立する”を表したLTL式[]pをLTL2BAでNever Claim に変換すると

¶ ³

never { /* []p */

accept_init:

T0_init:

if

:: ((p)) -> goto T0_init fi;

µ} ´

となる．

Never Claim内で使用する命題記号の定義は，LMNtalルールのように Symbol=Head :- Guard|

(25)

3.3 LTLモデル検査の実行方法 16 と記述する．命題記号の定義は1行に1つずつ行い，複数の命題記号を定義する場合は改行する．命題記号の名前をSymbolに記述し，LMNtalのルールにおけるヘッドとガードと同じようにHeadとGuardを記述する．なお，ガード条件が必要ない場合は記述を省略することができる．このHeadとGuardで記述されたLMNtalのルールがマッチするならば命題は真となり，しなければ偽となる．例えば，命題記号名pを“アトムaがあり，リンク先はground型である” と定義するには

¶ ³

p = a(X) :- ground(X) |

µ ´

と記述する．例えばa(b(c))が存在すれば命題記号のルールがマッチするため，命題pは真となる．

このように記述した Never Claim内で使用する命題記号の定義ファイルと，検証したい性質のLTL式を変換したNever Claimファイルを検査対象のLMNtalプログラムファイルと共にモデル検査器SLIMに与えることでLTLモデル検査を行うことができる．このモデル検査の流れを図3.1に示す．

図3.1 LMNtalにおけるLTLモデル検査の流れ

LMNtalモデル検査器SLIMは，検証対象の LMNtalプログラムのルール適用と，性

質オートマトンの状態遷移とを交互に行うことで，実行を進めつつ状態遷移グラフを生成する．探索はSPINでも用いられているnested DFSで行い，探索中に受理サイクルが見つかった場合はそこまでの経路を反例として出力する．

なお，LaViTでは1つのインターフェースでLTL式の記述と命題記号の定義をするこ

とができ，ファイルの生成も自動で行う．詳しくは4章で紹介する．

(26)

3.4 LTLモデル検査の実行例 17

3.4 LTL モデル検査の実行例

ここでは簡単なLMNtalの例題に対してにLTLモデル検査を行う．アトムnにリンクした整数アトムを書え換えていくLMNtalプログラムを以下に示す．

¶ ³

n(1).

n(N) :- N<5,M=N+1 | n(M).

n(N) :- N<5,M=N+2 | n(M).

n(N) :- N>=5 | n(1).

µ ´

アトムnに接続された整数アトムが5未満なら1ずつ増やすルールと，2ずつ増やすルール，5以上ならば1にするルールの3ルールがある．次に命題記号p, q, rを定義する．

¶ ³

p = n(N) :- N>0 | q = n(5)

r = n(1)

µ ´

アトムnに接続された整数アトムが 0より大きければ命題pは真に，整数アトムが5ならば命題qは真に，整数アトムが1ならば命題rは真に定義した．

ここで“アトムnに接続された整数アトムは，常に正の整数アトムである” であることを調べるためにLTL式[]pの否定をNever Claimに変換して検査を行うと

¶ ³

No Accepting Cycle (or Invalid State) exists.

’# of States’(stored) = 6.

’# of States’(end) = 0.

’# of States’(invalid) = 0.

µ ´

とエラーは検出されない．

次に“アトムnに接続された整数アトムは，必ずいつか5になる”の仕様[]<>qを満たすか調べると

(27)

3.5 非決定実行機能 18

¶ ³

CounterExamplePaths 1::T0_init{n(1). @5. }

* 4::accept_S2{n(2). @5. } 6::accept_S2{n(4). @5. } 8::accept_S2{n(6). @5. } 9::accept_S2{n(1). @5. }

* 4::accept_S2{n(2). @5. }

µ ´

と，エラーサイクルが検出され，整数アトムが5にならないサイクルがあることがわかる．

さらに“アトムnに接続された整数アトムは，必ずいつか1になる” の仕様[]<>rを満たすか調べると

¶ ³

No Accepting Cycle (or Invalid State) exists.

µ ´

と，整数アトムは必ずいつか1になることがわかる．

3.5 非決定実行機能

モデル検査器SLIMはLMNtalプログラムの全実行経路を出力する機能も備えている．

この機能は非決定実行機能と呼ばれる．例えば3.4節で前述したLMNtalプログラム

¶ ³

n(1).

n(N) :- N<5,M=N+1 | n(M).

n(N) :- N<5,M=N+2 | n(M).

n(N) :- N>=5 | n(1).

µ ´

のLMNtal プログラムは，加算の方法によって様々な実行経路を取り得る．このプログ

(28)

3.5 非決定実行機能 19 ラムに対してSLIMの非決定実行機能を用いると

¶ ³

States 6::n(6).

5::n(5).

4::n(4).

2::n(2).

3::n(3).

1::n(1).

Transitions init:1 6::1 5::1 4::5,6 2::3,4 3::4,5 1::2,3

µ ´

の出力が得られる．

States以下では

状態番号::状態のテキスト表現

の表記により，番号とLMNtalの状態の対応付けを行い，Transitions以下では状態番号::遷移先の状態番号のリスト

の表記により，遷移の情報を表示している．またinitが初期状態番号を示す．これにより全実行経路を把握することができる．

全状態数が有限であれば通常の実行では停止しないプログラムであってもLTLモデル検査および非決定実行機能は必ず停止する．

(29)

20

第 4 _章

LMNtal _{統合開発環境} LaViT _の

構成

LaViTが実装した機能は大きく分けて4つに分類される．

• ^{開発支援機能}

処理系仲介インターフェースとLMNtal専用エディタ

• ^{検証支援機能}

LMNtalモデル検査器の操作性を高めるLTLモデル検査インターフェース

• ^{検証評価機能}

モデルに対するLMNtalモデル検査器の性能を定量的に示すグラフビューア

• ^{検証可視化機能}

システムの性質を視覚的に表現するインタラクティブな検証ビジュアルツール本章では主に開発支援機能，検証支援機能，検証評価機能について紹介し，検証可視化機能は6章で紹介する．なお，バージョン2.4.2時のLaViTをもとに紹介する．LaViTの使用例を図4.1に示す．

4.1 LaViT 構成概要

LaViTの構成概要を図4.2に示す．LaViTは

• JavaによるLMNtal実行時処理系とLMNtalコンパイラ

• ^{モデル検査器}SLIM

(30)

4.2 開発支援機能 21

図4.1 LaViTの開発支援機能

• LMNtalプログラム実行可視化ツールUNYO UNYO

• LTLからNever Claimへ変換するLTL2BA

の処理系を 1 つのユーザーインターフェースで操作できるようになっている．公開版

LaViT^*1をダウンロードすると，LTL2BA以外の処理系が同封されており，環境でコン

パイルが必要なSLIMなどのインストールをLaViTは自動で行う．

4.2 開発支援機能

LaViTのウィンドウの左部分がLMNtalプログラムを編集するエディタ部，右半分が

タブで切り替えができる機能部である．

エディタ部の上部でプログラムを編集することができる．ここでは LMNtalプログラムを解析し“int”などの予約語やコメントを色付けを行い，プログラムの記述性・可読性を向上させている．

エディタ部の下部のボタンで処理系を実行することができる．各ボタンの動作を表4.1 に示す．

図4.1に示されている機能部ではSystemタブが選択されており，上部では処理系から

*1http://www.ueda.info.waseda.ac.jp/lmntal/

(31)

4.3 検証支援機能 22

図4.2 LaViTと他処理系の構成

の出力を，下部ではLaViTのシステム動作のログをそれぞれ表示している．上部のテキストには検索機能がついており，大量の出力が表示され可読性の悪くなった場合でもアトム名などでテキスト検索できる．下部のログでは処理系を実行する際のオプションなどを表示しているため，バックエンドでどのような処理が行っているかを確認することができ

る．またLMNtal処理系の概算実行時間の表示もするため，時間のかかる処理を行った

場合でも容易に実行時間を知ることができる．プログラムエディター，処理系実行ボタン，出力表示，ログ表示を1つのウィンドウにまとめることでスムーズな開発が行えるように考慮した．

4.3 検証支援機能

機能部をLTL記述用に切り替えて，3章で説明したLTL式の記述と式中で使用した命題記号の定義の記述の画面を図4.3 に示す．自動的に記述した内容のファイルが生成され，下部のLoadとSaveボタンで LTL式と命題記号の定義をセットで読み込みと保存ができるようになっている．LTL式を変換する LTL2BAはLTL式の入力部分の横にあ

るTranslate ボタンで起動することができる．LTL2BAはサイトからダウンロードし所

(32)

4.4 検証評価機能 StateProﬁler 23 ボタンのラベル説明

LMNtal(Java) JavaによるLMNtal実行時処理系でエディタ部のプログラムを通常実行する

UNYO(2G) JavaによるLMNtal実行時処理系に組み込まれている古い

バージョンのUNYO UNYOでプログラムを可視化する

UNYO(3G) 外部化され高機能化した UNYO UNYO でプログラムを可

視化する

StateProﬁler プログラムに対して検証評価機能StateProﬁlerを実行する SLIM モデル検査器SLIMで通常実行を行う

StateViewer 検証可視化機能StateViewerでモデルの動作を可視化する Kill 実行中の他処理系の動作を止める

表4.1 処理系操作ボタンの説明

定のディレクトリに置くと，Translate ボタンを押す際にLaViTが自動でインストールを行うようになっている．モデル検査器SLIMを実行する際もオプションにファイルのパスを自動的に指定するため，ユーザーはファイルの操作を意識せずにモデル検査を行うことができる．

4.4 検証評価機能 StateProﬁler

LMNtalモデル検査では状態の同型性判定に時間がかかることが多く，モデルの性質に

よって状態空間の探索にかかる時間が大きく異なる．また，反例を見つけるかすべての状態の探索が終了するまで定量的な出力は無いため，時間がかかる大きいモデルはモデル検査が進行しているか分からず，検査の実行速度を評価する方法も無かった．

そこで LaViTはモデル検査器の状態展開速度を測定する機能を備えた．この機能を

StateProﬁlerと呼ぶ．自然数アトムを生成するLMNtalプログラム

¶ ³

c(1).

c(N) :- N<4000,M=N+1 | c(M),n(N).

µ ´

にStateProﬁlerを実行した結果を図4.4に示す．X軸が時間軸，Y 軸が状態数を表し，

モデル検査器が展開した状態数を逐一プロットする．グラフの上部では展開直後の状態の

(33)

4.4 検証評価機能 StateProﬁler 24

図4.3 検証支援機能のインターフェース

LMNtal構造をテキストで表示している．このLMNtalプログラムでは展開ごとに 1状

態のアトムが1つずつ増えていくため，状態の同型性判定に時間がかかるようになり展開速度が遅くなっていくことがわかる．

またLMNtalモデル検査で無限状態空間の探索を行うと停止しないが，StateProﬁler

は誤って無限状態になってしまうプログラムを書いてしまったときもデバッグに使用できる．また無限でなくとも莫大な状態空間になってしまうプログラムの性質を見ることができる．整数アトムを無制限にインクリメントするLMNtalプログラム

¶ ³

c(1).

c(N) :- M=N+1 | c(M).

µ ´

にStateProﬁlerを実行した結果を図 4.5に示す．探索が停止しないプログラムにおいて

も，展開しているLMNtal構造を知ることができるためどのような状態展開が行われているかユーザーは把握することができる．

(34)

4.4 検証評価機能 StateProﬁler 25

図4.4 有限状態モデルに対するStateProﬁlerの実行

図4.5 無限状態モデルに対するStateProﬁlerの実行

(35)

26

第 5 _章

統合開発環境 LaViT _{の設計と実装}

本章では前章で説明したLMNtal統合開発環境LaViTの設計と，それに基づく実装について述べる．検証ビジュアルツールStateViewerの設計と実装は前章同様7章で紹介する．

5.1 統合開発環境 LaViT の設計

LaViTの設計にあたって以下の事に特に注意した．

• LMNtalを取り巻く処理系は多方面に独自の拡張がされる

• 1つのソフトウェア LaViTとして操作できるようにし，処理系の分断を可能な限りユーザーに意識させないようにする

• GUIの特性を活かしたLaViTとしての独自機能を提供する

• LaViT自体の機能や他処理系の機能は些細なものであっても使えるようにして

ユーザーの選択肢を広げる

ただし機能連携の多さから他機能に影響を与えるような不安性があるものは取り除き，

ユーザーに提供しない公開方針をとっている．

5.1.1 LaViT と他処理系の構成設計

LMNtalにはプログラム実行可視化ツールUNYO UNYOやモデル検査器SLIMなど

いくつかの処理系が存在し多彩な機能を提供している．他処理系の構造を図5.1に示す．

これらのシステムはその目的に合わせて適した言語が選択され設計と実装がされた．その

(36)

5.1 統合開発環境LaViTの設計 27

図5.1 LaViTが使用する他処理系の構造

結果，処理系の導入や実行方法が煩雑になってしまい，ユーザーが機能を十分に使い切れなくなってしまった．

そこでLaViTはLMNtalにおける開発や他処理系を操作の障壁をできるだけ少なくす

るため，公開版のLaViTと一緒に可視化ツールやモデル検査器を同封し，インストールもすべてGUI上で行えるようにした．また他処理系は同封されLaViTと連携するものの可能な限り他処理系の活発な開発に影響がないようにするため，標準入出力でのデータのやり取りを行うようにした．この結合度を低く保つ設計により，同封されている他処理

系はLaViTに依存することなく単独で動作させることも可能になっている．

5.1.2 LaViT のインターフェース設計

可視化ツールやモデル検査器を起動するためのコマンドなどは極力入力せず，ボタンだけで直感的に操作できるように設計した．これによりプログラマがLMNtalプログラムの記述に集中できるようにし，他処理系の操作方法を極力意識をしなくて良いようになっている．

LaViT上のウィンドウの概要を図5.2に示す．エディタ部と機能部はプログラマの意

図に応じて自由に領域を変えることができる．機能部はタブになっており，どの機能を使うかに応じて切替が可能になっている．タブ内はそれぞれの機能が目的に応じて集まるように配置を行い，タブの切替が最低限で済むようにしている．また例えば処理系起動ボタンでStateViewerを起動するとタブがStateViewerタブに自動で切り替わるように，実行した処理系の機能に応じて自動で適切なタブに切り替わるようにした．

(37)

5.2 統合開発環境LaViTの実装 28

図5.2 LaViTのインターフェース構造

5.2 統合開発環境 LaViT の実装

LaViTは

• ^{連携すべき}LMNtal処理系とUNYO UNYOがJavaで実装されている

• JavaのSwingによってユーザーが使いやすいGUIの実装が行える

• Windows,Mac,Linuxなど幅広い環境で動作させる

の理由から Java によって実装された．他処理系の実装言語については表 5.1に示す．

LaViTはオープンソース^*1で開発されている．ソースファイルの一覧を付録B.1に示す．

2009年から実装が行われ，バージョン2.4.2まで 45回のバージョンアップが行われた．

バージョンアップの内容を付録C.1に示す．

5.2.1 LaViT と他処理系の結合部の実装

既に示した図4.2にあるように，JavaによるLMNtal処理系にはLmntalRunner，SLIM にはSlimRunner，UNYO UNYOにはUnyoRunner，LTL2BAにはLtl2baRunnerが仲介役として存在し，これらのクラスによって処理系をカプセル化して起動している．各種

*1http://code.google.com/p/lavit/

(38)

5.2 統合開発環境LaViTの実装 29

処理系名機能実装言語

JavaによるLMNtal処理系実行時処理系，コンパイラ Java

UNYO UNYO LMNtal実行可視化ツール Java

SLIM 軽量高速な実行時処理系，モデル検査器 C言語

LaViT 統合開発環境，検証ビジュアルツール Java

表5.1 LMNtal処理系の実装言語

Runnerは実行開始時に呼び出すのrun()メソッド，終了判定するためののisRunning() メソッド，実行が成功したか判定するためのisSuccess()メソッド，実行を中断するため

のkill()メソッドを実装している．またそのRunnerの特性に応じて，実行時間を得る実

装や，出力の取得方法を変更する実装などがなされている．さらに各種処理系はThered を起動するため，LaViTの操作とは同期実行する事も非同期実行することもが可能になっており，ユーザーがスムーズに処理系を起動できる実装の工夫がなされている．

5.2.2 エディタ部の実装

エディタ部はユーザーの使用頻度が高い機能であると予想されるため，試行錯誤しながら実装を繰り返し行った．読み込みや新規保存，上書き保存などファイルの基本的な操作はもちろん，コピー，カット，ペースト，元に戻す(Undo)，やり直し(Redo)などの機能を提供した．またデバッグ時に役に立つよう行番号の表示も行っている．さらにLMNtal のプログラミングをし易くするために，“int”や“ground”といったLMNtalの予約語やコメントを色付けする機能も備えている．特にLMNtal プログラム色付け機能と元に戻

す(Undo)，やり直し(Redo)は相互に影響を及ぼすため実装を工夫している．ユーザー

の入力とプログラムの色付けを区別して履歴として持ち，元に戻す動作ややり直し動作をする場合はその履歴に基づいて色付けはスキップするように実装している．これによりユーザーが元に戻す，またはやり直す際に色付け動作だけが対象にならないようにし，

ユーザーの意図する履歴まで遡ることができる．

(39)

30

第 6 _章

検証ビジュアルツール

StateViewer _の構成

StateViewerが実装した機能は大きく分けて8つに分類される．

• ^{状態配置機能}

遷移を考慮した状態配置や，遷移をバネに見立てた力学モデルの適用による配置を行う

• ^{交差数削減機能}

遷移と遷移の交差を削減する

• ^{ダミーノード機能}

ダミーノードを導入することで状態と遷移の重なりを回避する

• ^{状態集合抽象化機能}

状態の集合を１状態に抽象化しブラウジングする状態数の削減を行う

• 実行シミュレーション機能

ユーザーが適用ルール，遷移先状態を選択し仮想的にLMNtal通常実行を１ステップずつ進めることで実行経路を確認できる

• ^検索機能

状態や遷移の検索を行う

• 3D状態遷移描画機能

Java3Dを使用して3次元上に状態遷移グラフを描画する

• LTL StateViewer

モデル検査器の検証結果をStateViewerで描画する

(40)

6.1 StateViewerの基本機能 31 本章では実行例を示しながらこれらの機能を説明する．

またControl Buttonタブの各ボタンや各チェックボックスの動作を表6.1と表6.2に，

Otherタブの各ボタンや各チェックボックスの動作を表6.3に，Windowsにおける右ク

リック時に表示される機能の動作を表6.4に，マウスとキーボードによる動作を表6.5にそれぞれ示す．

6.1 StateViewer の基本機能

図6.1 StateViewer実行例の全体図

StateViewerはLMNtalモデル検査器SLIMから得られる状態遷移の情報を解析し可視化を行う．単純に描画をするだけでなく，インタラクティブにモデルを検査するための機能をGUIで提供した．StateViewerの実行例を図6.1に示す．

1つの円がプログラムの1つの状態を表し，矢印が状態の遷移を表している．状態を表す円をクリックすると状態の内容をテキスト表示させることができる．また状態の色は遷移数と被遷移数によって決定される．特に被遷移数が0の初期状態は青，遷移数が0となる最終状態は赤で表示される．これにより最終状態などの状態遷移グラフにおいて重要な状態の発見をしやすくなっている．

(41)

6.2 状態配置機能 32

6.2 状態配置機能

StateViewerの状態配置機能は

• 遷移関係にある状態の平均Y座標に配置(Adjust Reset機能)

• ノードを反発物体に，遷移をバネに見立てた力学モデルによる配置

に大きく分かれる．ただし，ダミーノードの導入タイミングによって状態遷移グラフの形も変わってくる．また探索の深さを自然に表現するために状態遷移グラフのx 座標は状態の深さによって等間隔に並ぶように固定し，配置機能によって変化することがないようにした．

LMNtalによるλ計算のエンコーディング[21]でChurch数表現による2の2乗を計

算し，StateViewerで状態遷移グラフを表示したものを図6.2 に示す．このグラフに対

してAdjust Reset機能を実行したものを図6.3に示す．さらに力学モデルによる配置を

行ったものを図6.4に示す．Adjust Reset機能でも力学モデルによる配置でも最終状態が二つ存在すること，両最終状態に至るステップ数が異なることなどがはっきりと観察することができる．

次に円盤6枚のハノイの塔のプログラム

¶ ³

poles([p([1,2,3,4,5,6,999]),p([999]),p([999])]).

p@@ P1=p([H1|T1]), P2=p([H2|T2]) :- H1<H2 | P1=p(T1), P2=p([H1,H2|T2]).

µ ´

の状態遷移グラフを図6.6に示す．この図から再帰的な構造があることが予想できるが自明ではない．このグラフに対してAdjust Reset機能を実行(図6.7)すると，再帰的な構造を見て取ることができる．さらに力学モデルによる配置(図6.8)を行うと交差もなく再帰的な構造を完全に見て取ることができる．

ハノイの塔の状態遷移グラフでは力学モデルによる配置が優位であったが必ずしもそうとは限らない．例としては水差しの問題が挙げられる．ソースコードを付録A.1.1に添付している．初期配置(図6.9)から Adjust Reset機能を実行 (図6.10)すると対称性が見えるが．力学モデルによる配置(図6.11)を行うとその対称性が崩れてしまう．そのため

StateViewerは1つの配置方法だけの採用ではなく，ユーザーが意図に応じて配置方法を

変えることができるようにしている．

(42)

6.3 交差数削減機能，ダミーノード機能 33

6.3 交差数削減機能，ダミーノード機能

StateViewerはユーザーが正確に状態遷移グラフを理解できるように遷移と遷移の交差

を削減する交差数削減機能，遷移と遷移，遷移と状態の重なりを削減するダミーノード機能を提供している[13]．

水差しの問題の状態遷移グラフにAdjust Reset機能を実行(図6.10)したものに対してダミーノードを入れると図6.12のようになる．遷移と遷移の重なりが少なくなり，遷移先の状態が明確にわかるようになる．さらに交差数削減機能を適用したものを6.13に示す．交差が少なくなることで遷移がはっきりと把握し易くなる．

Adjust Reset機能を適用後，ダミーを導入し，交差数削減を実行する一連の流れを1

つにまとめた機能がDummy Mix Adjustとなっている．

またダミーノードの導入は深さ dの状態が深さd−n(n >= 2)への遷移(バッグエッジ)をもつ場合に挿入される Set Back Dummy機能だけでなく，同深度のノードで遷移と状態が重なっている場合にダミーノードを挿入して回避するSet Vertical Dummy機能も用意されている．例えばLMNtalプログラム

¶ ³

n(1).

n(N) :- N=\=1 | n(1).

n(N) :- N=\=2 | n(2).

n(N) :- N=\=3 | n(3).

n(N) :- N=\=4 | n(4).

µ ´

をStateViewerで実行すると図 6.14となる．実際には一番上のノードから一番下への

ノードへの遷移が存在するが，遷移が重なってしまい表現されていない．そこで Set

Vertical Dummy機能を実行すると，図6.15のように同深度の遷移と状態の重なりを避

けるためのダミーが自動で挿入され重なりを回避する．

6.4 状態集合抽象化機能

状態数の多いモデルはブラウジングや描画に限界があり，システムの挙動の理解が困難な場合が多い．そこでStateViewerは複数の状態を1状態として表示する抽象化機能を備えている．その抽象化対象になる状態集合は

(43)

6.5 実行シミュレーション機能 34

• ルール名を選択してそのルールで遷移可能な状態(Transition Abstraction)

• 直接マウスで選択した状態(Select Abstraction) の2パターン用意している．

特にユーザーの選択したLMNtalルールで到達可能な状態集合を対象に抽象化を行うことで，0ステップで遷移したように見せることができる．つまりユーザーが描画不要と

判断したLMNtalルールを描画対象から外すことができる．例として図 6.2に対してλ

計算のベータ簡約以外のLMNtalルールで抽象化したものを図6.5に示す．複数の状態をまとめた抽象化状態は四角で表している．その四角の状態をダブルクリックすると抽象化対象となった状態集合の状態遷移グラフを独立して表示することができる．これにより規模の大きくなった状態遷移グラフでも，抽象化機能を適用することで情報量を減らさずにブラウジングが容易になる状態数まで描画対象を削減することができる．

6.5 実行シミュレーション機能

状態遷移グラフがもつ情報を用いて仮想的にLMNtal通常実行を1ステップずつ進め，

実行する様子を再現する実行シミュレーション機能をStateViewerは備える．実行例を図6.17に示す．

start ボタンでシミュレーションを開始し，表示されている遷移先の状態を見ながら

適用したいルールを選択する．forwardにあるボタンが先に進むルール適用のボタンで，

backにあるボタンが戻るルール適応のボタンであり，深さが同じ場合はY座標が大きい遷移先状態順にボタンが並んでいる．ルールを適応するとグラフ上でも選択している状態が移動し，状態のテキスト表示が適応した順に記録されていく．

自動選択機能(Auto Run)も実装しており，通常は一番上のボタンが自動で選択され実行が進む．またルールに優先順位をつけて，順位が高いものから順に選択させることもできる．選択スピードも0.1秒から2秒の間で選択可能で，把握できる速度に調節できる．

このシミュレーション機能により，ユーザーはプログラムの実際の振舞をルール選択しながら確認することができる．

6.6 検索機能

状態を検索しマッチした状態だけを強調表示することもできる．例として水差しの問題を考える．

(44)

6.7 3D状態遷移描画機能 35 図6.9から図6.13までで示した状態遷移グラフは300mlと400mlの水差しで測れる水の全状態の構造を持っているため，ここから200mlの状態があるか調べれば良い．実際に200mlの水差しの状態があるか調べるため Headはjug(200, N),$pとし，Gurad は N >0で検索するとマッチする状態が図6.18のように強調表示される．よって200mlを測ることは可能とわかり，初期状態から強調表示されている状態までのパスが解となる．

また状態だけでなく遷移の検索もできる．遷移先，遷移元の関係からの検索とルール名による検索をサポートしている．例えば水差しの問題において “水をいっぱいにする” ルールﬁllで行われる遷移を強調したものが図6.19である．これによりルールﬁllでは初期状態に戻らないなどの遷移の特徴を把握することができる．

6.7 3D 状態遷移描画機能

StateViewerの描画力を上げるために，Java3Dによる3次元空間での状態遷移グラフのブラウジングをサポートしている．StateViewerと同様，クリックするとその状態の内容をテキストで表示する．また3D StateViewer で選択した状態はStateViewerでも選択されるようになっている．

6.3節で挙げた例題に対して3D StateViewerを適用したものを図6.16に示す．6.3節では遷移同士の重なりを避けるためにダミーノードを導入していたが，3次元であるため遷移同士の重なりは空間上では発生せず，正確にブラウジングできる．

検索の結果表示にも対応しており，6.6節で行った200mlが測れている状態の検索結果を3D StateViewerで表示したものを図6.20に示す．

簡単なLMNtalプログラム

¶ ³

n(1,a).

n(1,b).

n(1,c).

n(N,Atm) :- M=N+1,M=<3 | n(M,Atm).

µ ´

を通常のStateViewerで実行すると図6.21のようになる．ここからは規則性などはすぐ

に見て取れないが，3D StateViewerで図6.22のようにブラウジングするとこの状態遷移グラフは正六面体になっていることがわかる．このように通常のStateViewerでは発見できないような規則性や対称性が3D StateViewerによって見つけることができるようになった．

(45)

6.8 LTL StateViewer 36

6.8 LTL StateViewer

StateViewerにはLTLモデル検査を行ったときの性質オートマトンとシステムオート

マトンとの同期積オートマトンの全探索経路を可視化し，モデル検査でのエラーサイクルを強調表示するLTL StateViewer機能が存在する．

ここで3.4節で実行したLTLモデル検査をLTL StateViewerで実行する．“アトムn に接続された整数アトムは，必ずいつか5になる” の仕様 []<>qを満たすか調べるとエラーサイクルが検出されていたが，これをLTL StateViewerで描画すると図6.23のようになる．同期積オートマトンの受理状態を二重の円で表し，エラーサイクルを強調している．またこれを3Dでも表示することができる．3Dで表示したエラーサイクル検出を図 6.24に示す．これらのエラーサイクルをブラウジングすることで，どのようなパスが反例となっているかテキストだけでなくStateViewer上でも確認することができる．

(46)

図6.2 初期配置(Church数2の2乗)

図6.3 Adjust Resetよる配置(Church数2の2乗)

図6.4 力学モデルによる配置(Church数2の2乗)

図6.5 抽象化機能の適用(Church数2の2乗)

(47)

図6.6 初期配置(ハノイの塔)

図6.7 Adjust Resetよる配置(ハノイの塔)

図6.8 力学モデルによる配置(ハノイの塔)

早稲田大学大学院 基幹理工学研究科 情報理工学専攻

2010 年度 修士論文

インタラクティブなモデルの検査を可能にする LMNtal ビジュアルツールの設計と実装

提出日： 2011 年 1 月 27 日 指導 ： 上田 和紀 教授

早稲田大学大学院 基幹理工学研究科 情報理工学専攻

学籍番号： 5109B003-7

綾野 貴之

概要

目次

図目次

表目次

第 1 章

はじめに

1.1 研究の背景と目的

1.2 関連研究

1.2.1 SPIN のユーザーインターフェース jSpin

1.2.2 モデル検査器 LTSA

1.3 本論文の構成

第 2 章

LMNtal 言語解説

2.1 LMNtal 言語の概要

2.1.1 LMNtal の構成要素

2.1.2 LMNtal 基本構文

2.1.3 ガード付きルール

2.1.4 省略構文

2.1.5 コメント

2.1.6 プログラム例

2.2 LMNtal 処理系

2.3 LMNtal プログラム実行可視化ツール

第 3 章

LMNtal モデル検査

3.1 モデル検査とは

3.2 LMNtal モデル検査器 SLIM

3.3 LTL モデル検査の実行方法

3.4 LTL モデル検査の実行例

3.5 非決定実行機能

第 4 章

LMNtal 統合開発環境 LaViT の

構成

4.1 LaViT 構成概要

4.2 開発支援機能

4.3 検証支援機能

4.4 検証評価機能 StateProﬁler

第 5 章

統合開発環境 LaViT の設計と実装

5.1 統合開発環境 LaViT の設計

5.1.1 LaViT と他処理系の構成設計

5.1.2 LaViT のインターフェース設計

5.2 統合開発環境 LaViT の実装

5.2.1 LaViT と他処理系の結合部の実装

5.2.2 エディタ部の実装

第 6 章

検証ビジュアルツール

StateViewer の構成

6.1 StateViewer の基本機能

6.2 状態配置機能

6.3 交差数削減機能，ダミーノード機能

6.4 状態集合抽象化機能

6.5 実行シミュレーション機能

6.6 検索機能

6.7 3D 状態遷移描画機能

6.8 LTL StateViewer

早稲田大学大学院基幹理工学研究科情報理工学専攻

2010 年度修士論文

提出日： 2011 年 1 月 27 日指導：上田和紀教授

早稲田大学大学院基幹理工学研究科情報理工学専攻

綾野貴之

第 1 _章

第 2 _章

LMNtal _言語解説

第 3 _章

LMNtal _{モデル検査}

第 4 _章

LMNtal _{統合開発環境} LaViT _の

第 5 _章

統合開発環境 LaViT _{の設計と実装}

第 6 _章

StateViewer _の構成