ソフトウェア・シンポジウム2019 in 熊本

データベース・アプリケーションへの実行時モデル検査導入手法の提案
宮永 照二(株) テクノネット
myngshj3@gmail.com

要旨

パフォーマンスやユーザビリティの改善をもたらす一方
で，ライフサイルのステージ間で知識の共有がなされな

情報システムの急速なかつ広範囲な普及に伴って，情いために，さまざまな問題を引き起こすことが報告され

報システムの製品の品質とプロセスの品質の両方においている [2]．

て，新たな適用方法が提案されている [2][3]．

レガシーシステムだけではなく，新規開発のシステム

情報システムは開発・運用プロセスにおいてライフサ

についても，レガシーシステムと同様にステージ間の知クルを持つが，このライフサイクル内の各工程間でシス識の共有がなされず，1st リリース経過後の 2nd リリー

テムに関する知識が共有されていないために様々な問題

ス，3rd リリース等の後期リリースで同様の問題が発生を引き起こしている [2]．特にシステムの重要な性質にすることが懸念される．

ついてテストすら完全にできない状態が存在することもこれらの問題の多くは，大規模化複雑化するシステム

報告されている [2]．

に対して，十分な要求や設計を吟味する時間が短くなる

このような状況でシステムの重要な性質を検証する技傾向があり，そのために，時間が経過するにつれて，ド術として，実行時モデル検査 (On-the-Fly Model Check-

キュメントとソースコードのギャップ，ドキュメントとing) がある [7] [9] [10]．

実際の実装のギャップやドキュメント自体の非存在など

本稿では，情報システムとくにデータベースアプリが発生することが原因となっており，多くの場合，テスケーションについて，実行時モデル検査を効果的に適用

トによる品質の担保すら困難な状況が発生している [2]．

する方法について提案する．

これは情報システムの製品としての品質が保たれていないだけではなく，開発プロセスの品質が担保されていないために発生している問題である．

1. はじめにさらに，現在は情報システムが社会インフラの 1 つとして認識されており，その信頼性や安全性という概念は

1.1. 情報システムにおける品質保証の状況

重要な意味をもつ．単に設計通りに動作するシステムを構築するというだけにとどまらず，フォールトトレラン

情報システムは，研究目的の一時限りの開発 (One-ト・フェールセーフなどの運用やメンテナンスのステー

Time) ではなく，ビジネス上の要求にもとづくシステム
開発ではその品質とコストと適用効果が考慮され，ある
一定のタイムスパンを設けてライフサイクルが設定される (システムに対してライフサイクルという言葉を用いていることについては，システム，ライフサイクル概念，システムライフサイクルステージ，システムライフ
サイクルの典型について，[4] にその概要が記載されている．)．特に長いライフサイクルをもつレガシーシス
テムでは，計算機資源やアプリケーションの拡張により

ジにおける信頼性や安全性を含んだトータルな品質が要求される [6]．

1.2. モチベーション
このような問題に対して，厳密なプロセスを経て，正しいソフトウェアを作る方法としてフォーマルメソッドがある [1] (ここでは正しいソフトウェアを仕様や想定通りの動作をするソフトウェアという意味で用いている)．

135

SEA

ソフトウェア・シンポジウム2019 in 熊本

フォーマルメソッドは数理的な技法を駆使して厳密なプための設計を分離しない，つまりに二度手間を排除し効

ロセスのもとに正しいプログラムを作成するための総合

率的にモデル検査を適用しようとする事例である．

的な技術であるが，その用途は単に正しいソフトウェア

UML の使用の有無に限らず，モデル検査のための設計プロセスは，追加の労力を課さず，なおかつ専門的な知識の習得を極力排除して導入することが望ましいが，
一般的なデータベース管理システムの機能を利用すると，比較的容易にシステムの動的な検証が可能である．そこ
で，データベースアプリケーションにフォーカスを当て，その構成や性質から，検証用のコードを追加する労力を極力抑えて，動的な検証，すなわち実行時モデル検査を実施する方法を考案した．
本稿では，その実現方式について述べる．

を系統的に作成するだけにとどまらず，システムとしての性質を検証するのにも適用できる [1]．(正確にはシス
テムの性質を検証するプロセスはソフトウェアの信頼性を保証するためのプロセスに組み込まれており，そのプ
ロセスに数理的な技法を適用している．)
情報システムはそれが大規模化複雑化すればするほど，仕様全体を把握することが困難であり，そのライフサイ
クルの各ステージ間で同じ知識を共有することはなおさ
ら困難である．
このような状況に対して，システムの安全性などの

2. データベース・アプリケーションの特徴

重要な性質を実行時に検証する方法として，モデル検査(Model Checking) がある．モデル検査は，検査対象のモデルを記述し，そのモデル上でシステムの重要な性質，
例えば起こり得ない状態や安全性を脅かしかねない状態，
あるいは重要な問題が発生した状態などを報告することによって，システムの品質向上に役立てることができる．
モデル検査は、システムがとりうる状態を網羅的にたどることにより、システムの重要な性質が満たされることを検証する手法であるが、検証対象のシステムの規模によっては大きな状態空間とそれら状態間のネットワーク
を構築する必要があるため、性能の問題が顕在化する．
特にこの性能の問題に対して，On-the-Fly モデル検査(On-the-Fly Model Checking) [9] [7] [8] が提案されており，現実のシステム開発へ適用する研究もされている[8]．
複雑なシステムをモデル検査するのに，On-the-Fly モ
デル検査はパワフルで有効な手法である [9]．On-the-Fly

2.1. リレーショナル・データベースとデータ構造
データベース・管理システムの４つの重要な特性，すなわち，ACID 特性 (Atomicity, Consistency, Isolation,

Durability) はデータベース管理システムが提供する最も重要な性質である．これらの性質は，いくつかの構造を保全した情報システムの開発を容易にしている．
データベース管理システムをアプリケーションの中心に位置づける大きな要因は，大きく分けて次の点に分類されると考えている．
1. データについて構造を保全した記録と抽出が可能
2. 大量データの扱いについて，性能のチューニングが容易
3. バックアップ・リストア・レプリケーション等の管理が容易

モデル検査は，状態空間とそのネットワークを構築しな
がら，性質の検証を実行する [9] [10]．設計の早期の検証ステージで大量のバグを検出することができるため，本質的に設計プロセスでの適用に向いている [9]．
モデル検査のような数理的な技法による検証プロセスを実際に導入する場合，コストが余計にかかるというデメリットが存在する [3] モデル検査を適用することによる品質の向上という大きなメリットを生かすためには，
通常のプロセスに自然と組み込まれているように適用されるのが好ましいと考えられる．たとえば，検証のための追加の労力を極力課さずに設計検証を行う方法として

UML により記述される設計をモデル検査する方法の研究があるが [5][8]，これらも検証のための設計と製造の

136

1. は，リレーショナル・データベースのように何かしら存在する実体（エンティティ）間の関係を保存し，満たすべき関係を破壊する操作をキャンセルできる．この性質は重要な点である．既約なエンティティとそれらの関係からなるオブジェクトを統一的に記述できるアドバ
ンテージは大きい．この構造は通常，静的な構造・リレー
ションを基本とする値の制約だけでなく，アプリケーショ
ンレベルの制約を与えることで構造を破壊するための起
こるアプリケーションエラーを回避できる．
2. は，大量データを扱うアプリケーションに対して，
特に個別のアルゴリズムの開発を行うことなく，性能をSEA

ソフトウェア・シンポジウム2019 in 熊本

改善することができる．実際には，その用途に応じて，

2.2. アプリケーションの仕様と有限オートマトン

キャッシュやインデックス等の構成を設定したり，検索のオプションの記述を追加することで，並列化等のアル

データベース・アプリケーションはその名のとおり，ゴリズムを用いて高速化をはかることができる．昨今のそのデータをデータベースに保存するアプリケーション

データベースは大量のデータを保存し再利用する用途がである．アプリケーションはデータベースの ACID 特性

多くなっており，それに対してデータ量に応じたアルゴの恩恵により，アプリケーションを効率的に開発するこ

リズムの切り替えはアプリケーションの仕様に影響を及とができる．特に構造を保全する機能を導入することにぼすため実施しがたい．データ構造やアプリケーション

より，重要なデータ構造の破壊をもたらす機会を除去すのアルゴリズムに影響を与えず，高速化をはかるためのることができる．
一方で，アプリケーションは有限状態機械とみること

チューニングの機能は重要である．

3. は，管理面の効率化に寄与する．データベースを
バックアップする主な理由は，障害発生時の復旧にある．
障害発生時にはバックアップ記録から，システムを安全裏に回復するための機能が必要である．
アプリケーションの品質にもっとも大きく影響するのは，やはり，1. データ構造の保全機能である．リレーショ
ナル・データベースは前述の通り，エンティティ間の関係を保持し，エンティティ間の参照関係や依存関係を記述することができる．さらに，その使い方次第では，参照数の制限等の制約の追加などにより，より高い表現力を与えることができる．
例えば，グラフの構造を考える．グラフは構造 G =(V, E) で与えられるが，最もシンプルな構造，すなわち頂点と辺の定義のみに基づく構造のみでは，任意のノード間に双方向の参照をもつグラフが記述される．しかし
一般に，アプリケーションの持つデータ構造は，例えばそれは木構造であったり，サイクルであったり，またループを持たないものであったりする．そこでは，単なるグ
ラフ G に対して，いくつかの制約を与えなければならない．しかもそれは，アプリケーションの実行のタイミ
ングで，部分グラフ G1 ⊂ G が，組み込まれた別の構造を持つことがある．単なる静的な制約では実現できない
これらの構造の保全機能は，シンプルなプログラムを組み込むことで事前に実装可能となる．組み込み可能な構造についていくつか例を以下に挙げる．

ができる．例えば，一般的な Web アプリケーションは

1. 連結グラフ：任意の 2 つのノードを結ぶパスが存在する

すると，このオートマトンは図 1 のような概観をもつ．

2.

複数の画面と画面の背後にある，GUI と分離された機能からなり，ユーザは画面に対して操作し画面を切り替えながら操作する．ある１つの画面とその背後にある意味のある機能の組を１つの単位として，なになに画面のなになに状態，などと名付けることによって，アプリケー
ションの状態と関連付けることができる．
アプリケーションを有限状態機械とみなしたとき，それをデータベース内にグラフ構造を保存する機能を用いて実装することはあまりないと考えられる．それは実現可能であり，そのようなニーズも存在するかもしれない
が，一般的にはアプリケーションの取りうる状態の全体をそのままデータベースに保存してなにかしらの機能を実現するために用いているとは考えづらい．
その一方で，有限状態機械を採用すれば，システムにその性質に対する高い表現力を与えることができる．ここで，有限状態機械の例として決定性有限オートマトン
を挙げる．決定性有限オートマトンの定義は以下のとおりである．

A = (Q, Σ, δ, q0 , F )．ここで，Q は状態の集合，Σ は文字の集合，δ は遷移関数，q0 は初期状態，F は受理状態である．
いま，このオートマトン A に対応するラベル関数 Lを以下のように定義する．

L : Q ∪ Σ → S ．ここで S は文の集合である．

いま，関数 L はオートマトンの取りうる状態や受け付

二分木：連結グラフであり，かつ，すべての頂点

ける文字から文への対応を与えるため，文 ϕ, ψ ∈ S にあv に対して，v を根とする辺は存在しないか，または存在すればその数は２であるる意味を与えることにより，プログラムのモデルである
このオートマトンに重要な意味を与えることができる．

S = L(Q) ∪ L(Σ) とする．L(s) はある状態 s ∈ Q に

3. サイクル：ある頂点 v から同じ頂点 v へのパスが存在する

対応する文であり，この文が状態 s で常に成り立つ式

137

SEA

ソフトウェア・シンポジウム2019 in 熊本u

表 3. 遷移テーブル (Transitions)av
remarks

s1

a1,2

s2

transition from v1 to v2

s2

a2,3

s3

transition from v2 to v3

·
·

·
·

·
·

···
···

図 1. ラベル付きオートマトンの概念図
表 4. 現在状態テーブル (CurrentState)sremarksであるとする．また，L(a) をある文字 a ∈ Σ に対応する文であり，この文が文字 a に対応するプログラム (命sxstate − x令) であるとすると，オートマトン A はある命令 L(a)を入力として状態遷移する状態遷移システムを表すとし，オートマトン A を非決定性オートマトンに拡張する

・遷移状態の参照制約: ∀t ∈ T ransitions ◦ t.u, t.v ∈States ∧ t.a ∈ Alphabetsと，このオートマトンは一般化非決定性有限オートマト

・現在状態のシングルトン性: ∥CurrenState∥ = 1

ン (Generalized Non-deterministic Finite Automaton:

以上で，GFNA の静的構造は完成する．このオートみなすことができる．さらに，L(a) を正規言語に限定

GNFA) を構成するとみなせる．

マトンが入力により状態遷移するには，状態遷移を発生

そこでいま，この GNFA を構成するための構造をリさせるための次の機能の記述が必要である．

レーショナル・データベースに与えるために，次のよう・遷移実行処理: doT ansition(a ∈ Alphabets)

なテーブルを定義する．

2.3. アプリケーションを実行時に検証する仕組み
表 1. 状態テーブル (States)slabel

前項で説明した構造をもつ GNFA は，ある状態 s ∈ S

s1

ϕ1のときに成り立つ文 L(s) を s で成り立つ式とみなす．まs2

ϕ2

た，ある文字 a ∈ Σ のときに成り立つ文 L(a) を状態遷移

·
·

···
···

の契機となる命令とみなす．この構造を利用すると，図 1
であらわされるオートマトンの実行は，ψ1 , ϕ1 , ψ2 , ϕ2 , ψ3という文のシーケンスを表示する．言い換えれば，一連の文 ψ1 , ϕ1 , ψ2 , ϕ2 , ψ3 はアプリケーションの動作シナリ
オとして定義される仕様の一つであり，このシナリオに基づいたアプリケーションの動作を検証することがで

表 2. 文字テーブル (Alphabets)
a
label

きる．

a1

ψ1

この例では，状態 s1 にあるときに文 ϕ1 を与えると，

a2

ψ2

状態 s2 に遷移し，さらにそのときに文 ϕ2 を与えると，状

·
·

···
···

態 s3 に遷移するというシナリオを与えることができる．
これはちょうど，状態 s1 , s2 , s3 をそれぞれ画面 1, 画
面 2, 画面 3 に対応させ，文 ϕ1 , ϕ2 をそれぞれイベント

1, イベント 2 に対応させると，前述のシナリオは，「画面
1 のときイベント 1 を発生させると画面 2 に遷移し，さらにそのときイベント 2 を発生させると画面 3 に遷移する」と言い換えることができ，操作仕様と対応付けられこのとき GNFA が矛盾なく構成される構造は以下の性質を満たす．
・状態のユニーク性: ∀s, t ∈ States◦s ̸= t → s.s ̸= t.s

138

SEA

ソフトウェア・シンポジウム2019 in 熊本

た仕様として記述することができる．この仕様は，オペへの書き込みを同時に行わないような制御がなされる．

レーションベースでかつ検証可能なため，先述したシス

そのために，同一領域への書き込みリクエストを同時にテムライフサイクルのステージ間における知識の共有を処理しないような方式を採用する．

促進する．

いま２つのプロセスを状態遷移機械で表現し，２つのアプリケーションを実行時に検証する仕組みとしては，
状態 s に対応する文 L(s) を状態 s に遷移完了したタイプロセスが同時に同じデータへの書き込みをしないかどうかを検証しようとする場合を考える．

ミングで評価し，それが真となるか偽となるかを判定すプロセス 1 とプロセス 2 の計算モデルをそれぞれ，る方法が考えられる．より具体的には，文 L(s) が表す

A1 = (Q1 , Σ1 , δ1 , q1,0 , F1 ), A2 = (Q2 , Σ2 , δ2 , q2,0 , F2 )とする．

SQL 文を実行し，その結果によって判定する方法が考えられる．
いま，Java や C#のようなオブジェクト指向言語で採用されている try〜catch ブロックによる例外捕捉のメ
カニズムの記法を導入し，状態遷移に伴う処理を以下のように記述したとする．
ψ1 , try{ϕ1 , ψ2 }catch{ϕ2 , ψ3 }この処理のシナリオは ψ1 , ϕ1 , ψ2 と ψ1 , ϕ1 , ϕ2 , ψ3 の 2
つである．

これらの並行プロセスのモデルをオートマトンの積∏A=
Ai を定義することであらわすことにする．こ
i

こで，
∏
∏
∏
∏ ∏
∏
Ai = ( Qi , (Σi ∪ {ϵ}),δi ,qi,0 ,
Fi )，
i
∏

δi =

i
i ∏ i
∏i
∏
Qi × (Σi ∪ {ϵ}) →
Qi

i

i

i

i

i

である．
いま，2 つのオートマトンがそれぞれの状態遷移のシー
ケンス，s0 , s1 , s2 , s3 , s0 と q0 , q1 , q2 , q0 を取るとして，

2.4. 一階述語論理と時相論理による性質の記述

図 2 のようなコンカレントな状態をとる並行システム
アプリケーションは一般的に，複数の異なる状態を取を考える．

るが，各状態においてアプリケーションのもつデータがある性質を示している場合を考えると，s → ∀o ∈ Objects ◦ o.pのような，ちょうど状態 s にあるとき，Objects のインスタンス o の性質 p を満たすというような一階述語論
理の記述ができる．
さらに，アプリケーションの性質の意味論としてに有限オートマトンによる定義を与えると，例えば，「ある状
態 s から，入力 a によってクリティカルな状態 sc に到達aする関係が存在する」という意味の到達可能関係 s ⇝ sc
を反例とする，時相論理式a□¬∀s∀a ◦ s ⇝ scを，有限オートマトンのもつ構造から検証することができる．この時相論理式の直感的な意味は，「どんな状態にあっても，どんな入力を与えても，状態 sc に到達す
ることはない」である．

図 2. コンカレントシステムの状態図の概要
いま，A1 と A2 の積をとった時，現れる状態の一つ(s3 , q2 ) は同時に書き込みが行われる状態であるとすると，この状態に到達しないこと，すなわち G¬(s3 , q2 ) を検証するのが，実行時モデル検査の役割の一つである．
ユーザ user と状態 state の組 (user, state) を保存し，集合 {(user, state)} に state = s3 なるエンティティと2.5. コンカレントシステムの検証

state = q2 なるエンティティが同時に存在しないこと，
すなわち一階述語論理式

マルチスレッドやマルチプロセスのシステムでは，複数のタスクが非同期に稼働する．分散処理においては，¬(∃u ◦ u.state = s3 ∧ ∃v ◦ v.state = q2 )ひとつのデータベースに複数のタスクが同時に書き込みを満たすかどうかで検証できるし，このような性質をを行うが，書き込みの衝突を回避するために，同じ領域保全するために，状態遷移が確定する直前に，この一階

139

SEA

ソフトウェア・シンポジウム2019 in 熊本

述語論理式が満たされない場合に，遷移をキャンセルす3. 状態２ s2 は，Enter キーイン待ち状態．状態２ s2は，ユーザが計算を実行可能な状態である．このモードに滞在するときは，演算キーインがあった場
合は s1 へ遷移し，クリアキーが入力されたときには s0 に遷移する．Enter キーインがあった場合は計算を実行し，s0 へ遷移する．

るといった処理を組み込むことで，安全にコンカレント
システムの競合回避機能を実装することができる．

3. ケーススタディ
3.1. 電卓 GUI アプリケーション

このアプリケーションの状態遷移システムは図 3 のようになる．

トイ問題として，電卓 GUI アプリケーションを例に挙げる．
このアプリケーションの仕様は以下のようである．
画面仕様：このプログラムは，１つのスクリーンからなり，数字：0,1,..,9 に対応するボタンと演算子:+,-,*,/に対応するボタンとクリアキー:C に対応するボタンとエンターキー:E に対応するボタンが配置されている．さらに，計算される式を画面に表示するための Widget と計算結果を画面に表示するための Widget からなる．
分析結果：電卓は一般的に，複数のキーを組み合わせて連続でキーインすることによって，計算したい式を指図 3. 電卓アプリの状態図

定する．さらに計算用のキーをキーインすることによって，計算を実行し，その計算結果を表示する．

設計にならって有限オートマトンを構成すると，以下計算式を指定するときには，計算式が適切な式になる
ように，キーインを受け付けるかどうかの制御を行う．

のようになる．

例えば，すべてのキーインをすなおに受け付けてしまう

Q = {s0 , s1 , s2 }と，計算式が例えば「３＋−２」となるような，算出不ΣN = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}可能な式を指定してしまう可能性があるために，入力状

ΣO = {+, −, ∗, /}態に応じてキーインを受け付けるかどうかの制御を行う．
この分析結果を反映した結果，設計は以下のように

ΣC = {C, E}Σ = ΣN ∪ ΣO ∪ ΣC ∪ {ϵ}なった．まず，このアプリケーションは以下の３つの状態を持ち，それぞれの状態からそれ自身または他の状態

δ = δs0 →s0 ∪ δs0 →s1 ∪ δs1 →s0 ∪ δs1 →s2 ∪ δs2 →s0へ遷移する．

q0 = s0
F = {s2 }1. 初期状態 s0 は，アプリケーションが立ち上がって最初の状態．初期状態 s0 は，ユーザがなんのアクションをしなくても，初期化処理の後に次の状態 s1に遷移する．

このとき検証したい性質は，Enter キーが受け付けられる場合には，計算式が適切であり計算可能な式を表している必要がある．いま計算式を µ とすると，µ は次のような正規表現のクラスに属する必要がある．

2. 状態１ s1 は，数字キーイン待ち状態．状態１ s1 は，ユーザが最初に数字を入力するモードである．ここで数字を入力するとモード変更し s2 に遷移する．演
算キーインは受け付けない．C キーを入力すると s0に遷移する．また，このモードに滞在するときは，Enter キーを受け付けない．

140

1 ∗
µ ∈ ((Σ+N ΣO ) ΣN )すなわち，このアプリケーションのもつ性質である，計算が正しく行われるための性質は，
1 ∗s2 → µ ∈ ((Σ+N ΣO ) ΣN )となる．実行時にこのような性質を検証することによって，仕様の検証を行うことができる．

SEA

ソフトウェア・シンポジウム2019 in 熊本

1. Step-1:ステートチャートから導き出される，静的に決定するオートマトンを構成する

3.2. 既存仕様の記述:個人情報更新処理
トイ問題としてネットバンキングの個人情報更新機

2. Step-2:ガード条件のすべての性質を CNF またはDNF に変換する能を考えてみる．この処理では図 4 のようなステート
チャートが想定される．

3. Step-3:時相論理に基づいて到達可能性判定を行う
4. Step-4:静的なオートマトンに対して，状態間の新たな遷移を追加したオートマトンを動的に構成する
5. Step-5:新しいオートマトンに対して性質を検証する
Step-4 と Step-5 を繰り返すことによって，On-theFly にオートマトンの構成とその上の性質の検証を同時に行う．
複雑なアプリケーションになればなるほど，静的な構
造はそれを適切にモデル化することが難しく，実際のプ
ログラムと乖離したモデルを作成してしまうことも往々に存在する．
実行時に，実際に実装された構造を構築するメリット
は，本来ある仕様記述の不備や，想定されない振る舞いを検証する機会を与える．
この場合，あるときに成立していた性質が，その後のあるときには成り立たないことが起こりうる（到達可能な経路が現れる）．そのため，オートマトンが構成されたタイミングで検証を行う．
本提案手法の，新規開発ではなく，リプレースや機能追加・改変への有効性・メリットは以下のことがあげられる．
1. プログラムのある状態で取りうる性質が変わることへ対応できる．

図 4. ネットバンキングのステートチャートの部
分図

2. ステートチャートと状態遷移表で直感的オペレー
ション仕様は推定できる．

このログイン (サインイン) に関する性質には以下の性質があげられる．

3. 状態を性質ベースで記述するため，プログラマレベ
ルで認識しているステートとユーザレベル認識ス
テートの乖離を減少させられる．

1. 有効なログイン状態である ≡ login
2. 有効なログイン状態にない ≡ ¬login

3.3. 機能追加:多重ログイン許可機能

3. Credential がマッチする ≡ pwd match

前述のバンキングシステムではログインユーザ 1 人に

4. Credential がマッチしない ≡ ¬pwd match

対するステートチャートを考慮していた．しかし実際には，複数のユーザが同時に操作する場合があり，場合にこのように定め，複雑な性質の記述を回避することによっては同時ログインしての作業を許す場合もある．

する．次にオートマトンを次のように構成する．

141

SEA

ソフトウェア・シンポジウム2019 in 熊本

4. ディスカッションと結論

そこで，多重ログインを許可するデータ構造を導入し，その際に想定される満たすべき性質を検証する例を考える．

4.1. ディスカッション

現行のログインユーザテーブルを仮定し，そこにユー
ザ ID とは別のクライアント ID を設けるように拡張し，
以下のような構造を与える．

本稿では，データベース・アプリケーションが状態遷
移機械とみなせる場合のシステムについて，実行時に時相論理や一階述語論理に基づくモデル検査を行い，シス
テムの安全性などの重要な性質が満たされるかどうかを検証する方法を提案した．

表 5. ログインユーザテーブル (LoginUsers)
userid clientid login time lastevent time

そのなかで，実際のケーススタディとして，電卓アプ
リケーションとコンカレントな操作が可能なネットバン

id1

client1login time

last event time

キングの例を説明し、さらに実際の開発の現場で実施さ

·
·

·
·

·
·

···
···

れる機能拡張に該当する同時ログイン機能追加を例にして，モデル検査の方法を説明した．いずれにしても，本稿では極めてシンプルで状態の数や遷移パターンが人手で数え上げられるほどであり，現実のシーンではもっと多くの状態や遷移パターンが現れることは必至である．

このような構造を導入しないと，次のようなことが起
こる．端末 A で操作しているときに，タイムアウトとな

さらに，検証すべき性質を満たすかどうかの式は一般

る時間が経過している．端末 B でログインして操作するに，一階述語論理式と時相論理式で表されるが，開発者と，タイムスタンプが更新される．端末 A での操作はタは，例えば単体テストを行うときには，SELECT 文でイムアウトのはずなのに，更新がかかっているために引必要なデータを抽出し，プログラムの正しい動作を検証

き続き作業ができてしまう．

するということを行うのが通常であろう．本稿の冒頭で述べたように，アプリケーションのもつ性質についての

これを検証するには，以下の式を検証する．

知識がステージ間で共有されていない現実に対応するた

ログインユーザのテーブル LoginU sers があって，あめには，適切に入力したり，問題をアラートするためのる userid = id1 のユーザが，clientid = client1 で実行

フロント機能の提供が必要と考える．

している場合を考える．その際のテーブルの構造として，

4.2. 提案手法のアドバンテージ(userid, clientid)) は主キーとなるように制約を与えられているとする．

本稿で述べた方式による利点は以下のものがあげら

C = CurrentStates = {(userid, clientid, state)} とすると，ある userid に対して個人情報の安全な書き込みが満たされる条件は，現在状態がクリティカルセクショ
ン Sc = P ersonalInf oSave に同時にないことであり，れる．

1. アプリケーションへの実装の影響を極力抑えて，検証を可能とする∀u ∈ LoginU sers◦

2. アプリケーションの実行時にシステム検証を行うことを可能とする∥{v ∈ C; v.userid = u.userid ∧ v.state = Sc }∥ ≤ 1を満たすことである．これが満たされている場合，同既に稼働しているシステムや，モデル検査等による設時にクリティカルセクション P ersonalInf oSave にな計検証を実施せずに実装しているシステムに対して検証

いために，同時に書き込みに入ることはない．したがっを行う方式であり，まだまだ新しい技術であるモデル検て同時保存の状態を回避することができる．万が一クリ査がコストを要する現状においては，本稿記載の方式はティカルセクションに同時に入ってしまった場合，実際

アドバンテージがあるといえる．
また，実装方式としては，静的な状態空間を作成せに入ってしまったことを ASSERTION で確認することず，オンデマンドに状態空間とネットワークを生成する

もできる．

142

SEA

ソフトウェア・シンポジウム2019 in 熊本∀r ∈ Record ◦ r.id = id → r.p

On-the-Fly 方式を採用することにより，アプリケーションの実行と同期的にモデル検査を実施するという方式を提供できる点もアドバンテージがあると考えられる．

なる性質の検証を基本的に行うようなメカニズムを提供するようにすれば，性能が向上すると考えられる．

この点については，今後試験実装を進めることにより，

4.4. 性質の認識と記述

本稿提案の方式の実用性を検証する必要がある．
本提案手法で懸念される問題は次項以降で説明する。

一般的にモデル検査は設計を検証するために行われており，既に製造された，あるいは製造中のシステムに対

4.3. 性能面の問題

して検証を行うには，別途検証用のモデルを作成する必データベース管理機能を検証のプラットフォームとし要がある．本稿で説明したような方式は，運用の点で以て利用するというアイデアは，実装の容易性や機能とし下のような課題があげられる．

ての有効性とは相反する性能の低下を招くおそれがある．

1. 性質をどこまで適切に記述できるのか

性能面の課題は以下のようなものがある．

2. 仕様としての正しさと想定外の振る舞いに対する対応をどうするか

1. 状態を記録するオーバーヘッドにどう対処するか
2. COMMIT によるブロックの発生による影響をどう抑えるか

性質をどこまで適切に記述できるのかという問題は，モデル検査で検証する性質の表現力の問題である．プロ

3. ネットワークトラフィックの増加にどう対処するか

グラマ目線で記述される検証式は、データ構造を熟知し状態を記録するためにおこるオーバーヘッド，状態をた状態の表現であり、単体テストで実行する検証式を流確実に記録させるための記述量の増加とそのために発用し、ステージ間で共有することを想定している．より生する処理が懸念材料である．また，COMMIT による汎用で一般的な性質の表現の可能性を探る必要がある．

ブロックの発生頻度も考慮しなければならない．多数の仕様としての正しさと想定外の振る舞いに対する対応

ユーザが利用するデータベースアプリケーションでは，は，完全な検証モデルの記述とトレードオフである．本ネットワークトラフィックの増加による検証への影響も

稿では時相論理式と一階述語論理式で与えらえる検証式

考慮しなければならない。これらの性能低下を和らげるを対象とする方針を示したが，時相論理で対象にするオ

方策の一つとして，On-the-Fly モデル検査を採用した．

ペレータは用途が広く，フルスペックの検証器を独自に

On-the-Fly モデル検査は、検証が必要なときに必要な状
態空間を生成するため，実行時のコストが低い．また状態遷移のタイミングで検証を行う必要があるが，複雑なアプリケーションや多数のユーザが協業するコンカレン
トシステムだと，これらのオーバーヘッドは避けられない．仕様理解やテスト等のステージでアプリケーション
を Run させることにより性質の検証を網羅的に行い，性能が要求されるステージでは特に重要な性質のみに絞って検証するようにすれば，性能の問題を回避できると考えている．

実装するには実現するためのコストがかかる．さらに効率よくモデル検査を実装する方法し、高い表現力を誇る方式を検討している．

5. 謝辞
本稿執筆にあたって，アドバイスをいただいたソフト
バンク株式会社の瀧本和弘氏，関係部署に調整いただいた株式会社テクノネットの原嶋麻衣子氏，および本稿を査読いただいた先生方にはこの場を借りてお礼申し上げます．

検証のタイミングでブロックが発生することに関して
は、例えば，集合演算を用いたデータベース管理システ

参考文献

ムの諸機能を，単一エンティティとそれに関連するエン
ティティに限定して操作するメカニズム，つまり∀r ∈ Record ◦ r.p[1] 中島 震, “ソフトウェア工学のツールとしての形式手法”, NII Technical Report, 2007.

という性質ではなく，

143

SEA

ソフトウェア・シンポジウム2019 in 熊本[2] 情報処理推進機構, “システム再構築を成功に導く
ユーザガイド”, SEC Books, 2016[3] 池田 信之, 今村 紀子, 高田 沙都子, “実用化に向けたモデル検査適用手法の開発”, 東芝レビュー, 2007
[4] IPA/SEC, “システムライフサイクルプロセス説明(案)”, システムズエンジニアリング推進 WG 参考
2(17-SEWG-2)[5] 岸 知二, “モデル検査技術にょる UML 設計検証”, 情報処理 2006 年 5 月[6] 向殿 政男, “信頼性と安全性”, SEC journal Vol.10
No.3[7] Jean-Michel Couvreur, “On-the-fly Verification ofLinear Temporal Logic”, FM 99, Vol. I, LNCS
1708, pp. 253–271, 1999.
[8] Stefania Gnesi, Franco Mazzanti, “On the fly model
checking of communicating UML State Machines”,
http://fmt.isti.cnr.it/WEBPAPER/ontheflySERA04.pdf[9] Ilan Beer, Shoham Ben-David, Avner Landver,“On-The-Fly Model Checking of RCTL Formulas”, Lecture Notes in Computer Science, Decembere 1999.
[10] R.Gerth, D.Peled, M.Y.Vardi, P.Wolper, “Simple
On-the-fly Automatic Verification of Linear Temporal Logic”, Proceedings of the 6th Symposium on
Logic in Computer Science

144

SEA