日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

自己適応システムの安全なコンポーネント置き換え
中島 震

Web アプリケーションに代表されるオープンなシステムでは，機能変更を柔軟に行う自己適応の方法を採用することがある．自己適応システムでは，実行時に構成コンポーネントを置き換えるので，このような置き換えが安全なことを確認しなければならない．本論文では，安全な置き換えの方法を論じる枠組みを提案し，さらに，インテグリ
ティに基づく検査法を提案する．具体的な応用例として，簡単な Web アプリケーション・システムを用いて，提案
方式を具体的に述べ，その有用性を論じる．

テムは，実行時に，置き換え後の動作を継続できるよ

1 はじめにうな適切な状態を設ける．自己適応アーキテクチャに

Web アプリケーションは，オープンなシステムで依存した方法が議論されている [17] [20] [28]．第 2 に，あり，常に変化するビジネスへ対応することが期待さ

置き換え前に満たしていた性質や制約条件を，置きれる [24]．一般に，開発時に，動作状況を含むシステ

換え後のコンポーネントが壊さないことを保証する．

ム要求を，完全に決めることは困難であり，サービ

このような置き換え可能性は，従来は，コンポーネン

スイン後にシステム要求が変化する [7]．このようなトの振る舞い等価性 [13] や振る舞いサブタイピング

オープンなシステムの構成法として，自己適応システ[16] によって定義していた. しかし，これらの方法で

ムが導入された．自身の実行状況や動作環境を監視す

は，置き換え後のコンポーネントの機能振る舞いが追ることで，振る舞いを実行時に変更する．現在，ソフ加的である．制約条件を壊すようなコンポーネントを

トウェア工学の主要な研究テーマ [3] となり，モデル

排除できない場合がある．置き換えるコンポーネント

ベース自己適応アーキテクチャ [4] [8] [18] [20] [26] や定の機能振る舞いが制限されたものであることを確認

量的な評価法 [10] [21] [25] の研究が進められている.

する新しい方法が必要になる．

自己適応システムは期待される柔軟さを実現する

本論文では，文献 [22] のアイデアを基に，コンポー

方法として，システム構成コンポーネントを実行時

ネント置き換え可能性検査の具体的な新しい方法を報に置き換える．コンポーネントを置き換えた後にも，告する．提案方法は，文献 [20] で述べた自己適応アー

アプリケーションシステム全体が支障なく作動しなけ

キテクチャの枠組みを踏襲し，インテグリティ・ポリ

ればならない．そこで，このようなコンポーネント置

シー [1] に基づく．本論文の成果は以下の 2 点に要約

き換えの安全性を確認する方法が必要になる．

できる．(a) 自己適応システムの置き換え可能性と従コンポーネントの安全な置き換えは，強く関連す来技術との違いを整理したこと，(b) 具体的な例としる 2 つの技術課題からなる．第 1 に，自己適応シスて Biba リング・インテグリティ・ポリシーに基づく
置き換え可能性が自己適応 Web アプリケーションでSafe Substitution of Components in Self-Adaptive Application Systems.
Shin Nakajima, 国立情報学研究所 / 総合研究大学院大学, National Institute of Informatics / SOKENDAI.

有用なことを示したこと，である．
以降，第 2 節は議論のもとになる自己適応 Web ア
プリケーションのフレームワークを紹介し，第 3 節では HTTP レスポンスの生成と共に全て失われる．しSPLE Method
Core
AssetsFeatureDiagram

たがって，長時間トランザクションを実現するには，
後続のプログラム実行に情報を引き継ぐ機構が必要(select) Reasoner
PHP
Files

HTTP Request(load)

Clients

PHP-based
Web Applicaon

図1WebServerPlaorm

MonitorAutomata

的で Web サーバが生成するクッキーと，データベースに格納するアプリケーション固有データを用いる．

(execute)
PHP
Programとなる．具体的には，利用者セッションを識別する目

Event
Generator

自己適応 Web アプリケーションのアーキテクチャ

これらのデータを利用して，一連の HTTP リクエス
トからなる長時間トランザクションの大域的な状態を管理する．
図 1 において, Event Generator はプログラム実

背景となる技術を説明する．第 4 節は置き換え可能性

行ステップ・レベルの情報をイベントに変換する．

を論じる枠組みを提案し，第 5 節で自己適応 Web アMonitor Automata はイベント列を監視し，条件違反

プリケーションへの具体的な適用事例を示す．第 6 節が起こるか否かを調べる．条件違反が発生した場合，

で関連研究と比較し，第 7 節でまとめの議論を行う.

その原因を求める．つまり，プログラム実行履歴という低レベルの情報を用いて，デザイン・レベルでの条

2 自己適応 Web アプリケーション

件違反を見つける．

自己適応 Web アプリケーション・アーキテクチャの例

Reasoner は条件違反を解決するのに必要なコン[20] を図 1 に示す．Monitor, Diagnoser, Reconﬁgura-

ポーネントを決定する．デザイン・レベル情報を基

tor からなるアーキテクチャ [4] を具体化したもので，に条件違反を防ぐプログラム・コンポーネント Core

Monitor, Analysis, Planning, Execution (MAPE)

Assets を求める．このプログラムは PHP ソースファループ [14] による方法が基本となる.

イルとして管理されている．Reasoner は求めたソー

Web アプリケーション・システムでは，クライア

スファイルをファイルシステム内の予め決められた場

ント側で，Web ブラウザを用いる．Web ブラウザは所に移動する．この新しく置かれたソースファイル

HTTP プロトコルによって，Web サーバに処理要求

は，以降，Web サーバにロードされて実行されるこを伝える．この要求は PHP 言語等で作成したサーバとになる．つまり，プログラムの置き換えは，予め決側プログラムを起動する．HTTP リクエストを受けめた名前を持つソースファイルを決められた箇所に移取ると，アプリケーション機能を実現するプログラム

動するだけで良い．

のファイルをサーバにロードして実行する．アプリ
ケーション・プログラムは MySQL 等のデータベー

3 準備スに格納されている永続データを利用する等によった

本論文の提案方式を説明する第 4 節に先だって，背処理を行った後，返却値となる HTML 文書を生成す

景となる知識を整理する．

る．この HTML 文書は Web ブラウザ上に表示され，利用者 GUI となる．

Web アプリケーションは，通常，連続した複数のHTTP コマンドを用いることで，興味深いアプリケー
ション・サービスを提供する．そのような典型例とし

3. 1 自己適応システムのフレームワーク
最初に，文献 [20] にしたがって，自己適応システムのフレームワークを紹介する．
適切さの規則 [11] は，一般に，システム要求とそれて，長時間トランザクションを用いる電子商取引 (ECを満たす仕様記述の関係を，D ∧ S ⇒ Rサイト) がある．ところが，HTTP プロトコルは状態る．ここで，R は要求，S は仕様記述あるいはシステと説明すを持たず， HTTP リクエストを受け取る度に，実行ムを表す．また，D はドメイン知識あるいはシステム

プログラムが初期化される．プログラムの実行状態に対する前提条件を示す．オープンなシステムでは，

(D1 || D2 ), S |= ∃rd .

利用者の振る舞いも含むと考える．適切さの規則をモ
デル論的な関係と見做す場合もあり，D, S |= R とこのようにシステムは rd を満たさないことから，品考える．R は要求性質を表す論理式の集まりである．

質保証という観点からは，好ましいものではない．逆文献 [9] では，ドメイン知識 D を，Df （固定) とに，上記の関係は，オープンなシステムで実行時干渉

Dc (変更可能) の 2 つに分割した. 本論文では，簡単が発生している状況を表すと考えることもできる．つに，Dc だけを考え，Dc と D を同一視する．この時，まり，rd が満たされないという実行時干渉を検知す

自己適応によるシステム変更は，次のような 2 つのる方法をロジック・モデル検査の問題と見做し，生成関係として表すことができる．ただし，X  は変更後した反例が原因を推定する情報を与えるのである．図の X を表すとする．

1 の Monitor Automata は，このような検査を行う．

D, S |= R,


D, S



実行時干渉あるいは不具合が検知された場合，ある


|= R.

R に対して以下の関係が成り立つように，自己適応システム S は S に変更されて (S;S と書く) ，D

システムは自身のシステム仕様あるいは機能振る舞の変化後であっても R が満たされることを示す．

いを変更する (S ; S  )．

文献 [20] は，この方法を拡張して，実行時干渉を説(D1 || D2 ), S  |= R .

明する枠組みを提案した．要求 R を個々の要求性質

R は R から作られるものであって, Rd を満たすよう

rk からなるとする．つまり，R =rk とする. 以下，に，Rf 中のいくつかの要求性質（{a}）を除去した

集合 R = { rk } と考えることもある. この時，適切ものである R = (Rf \{a})∪Rd . 変更後の S  が提供

さの規則は，D, S |= ∀rk という関係の集まりである.

する機能振る舞いは制限されたものであり，機能が縮

実行時干渉は，利用者の非決定的な振る舞いが原因退したと考えられる．

となって起こることがある [19]. || を（並行）結合オ

オープンなシステムでは，干渉の原因が消えるこ

ペレータとし，D が 2 つの要素の結合 (D1 || D2 ) として表されるとする†1 . この時，実行時干渉は，関係とがあり，この時，D は D に戻る．このような状況(D1 || D2 ), S |= ∃rj , と Di , S |= ∀rk (i = 1 か 2)

トがシステムへの攻撃を止めた場合などであろう．こが成り立つことと表せる.

のような場合，機能縮退しているシステムを元の振復帰が起こるのは，たとえば，悪意のあるクライアン

文献 [20] では，R を，さらに，R = Rf ∪Rd かつる舞いに復帰させたい（S  ; S ）. 上に述べた実行

Rf ∩Rd = φ，が成り立つように分割できる場合を考時干渉検知の方法を踏襲すると，適切な新しい検査

える. Rf は基本的な要求機能であり，Rd は導出機

性質を導入して，実行監視する必要がある．つまり，能である．Rd は高次ゴール [15] あるいはポリシー [6]R = (Rf \{a})∪(Rd ∪{b}) であって，b は状況復帰に関連し，Rf に対して冗長ともいえる．すなわち，検知を調べるのに必要な性質である．

Rd は高レベルの性質であって， Rf に含まれる基本

D, S  |= b.

的な機能を組み合わせて再現できる．システムの新

つまり，このような性質 b は D と S  の組み合わせにしい機能要求を表すものではない．つまり，rf ∈ Rf

対して満たされない.

と rd ∈ Rd に対して, 次のような関係が成り立つと考える．

D, S |= (rf ⇒rd ).

3. 2 置き換え可能性
置き換え可能性は，ソフトウェアシステム構築を柔

さらに，実行時干渉は，以下のような状況を表すと軟に行う基本的な技術として重要である．以下，置する．

き換え単位をコンポーネントと呼び，So あるいは Sn(D1 || D2 ), S |= ∀rf ,†1 議論を簡単にすることから 2 つに分解される場合を考える．

と表記する．特に，古いコンポーネント So を新しい
コンポーネント Sn に置き換える場合を考える. また，C[ · ]So を，コンポーネント So 実行の文脈とすると,

ここでの問題は，C[ Sn ]So が可能であることを表す

ム向けの新しい置き換え可能性規則を提案する．

形式的な記述と検査規則を求めることである．
置き換え可能性はソフトウェア構築法のに基本的

4. 1 置き換え可能性の枠組みな技術であり，従来から様々なアプローチが議論されWeb アプリケーションが，外部の変化に対応して，てきた．たとえば，VDM [12] のオペレーション・リ

自身の構成コンポーネントを置き換える場合を考える．

ファインメントは，抽象オペレーションを具体レベ

今，ϕ が要求性質を表す論理式とする．また，D と D

ル・オペレーションに置き換えることでオペレーショ

が外部環境を表し，D は D に変化する. 変化の前にン構築を段階的に行う方法である．ここで，オペレー

は，D, (S, So ) |= ϕ であり，システムはここでの議論

ションは，事前条件と事後条件の組として定義されに関わるコンポーネント So とそれ以外 S とからなる

る．リファインメントが正しいことの確認は，証明条とする. 変化が起きることで，D  , (S, So ) |= ϕ となる.

件（証明責務）が成り立つことを示すことによる．一次に，So を Sn に置き換えることで, D  , (S, Sn ) |= ϕ

方，オブジェクト指向プログラミングの振る舞いサが成り立つようにする. ここで，ϕ は，実行監視とい

ブタイプ [16] は，スーパータイプのインスタンス・オ

う観点から，第 3. 1 節で述べた rd の一例である.

ブジェクトをサブタイプのオブジェクトに置き換える

今，Sj 間の半順序関係を導入する．つまり，So Sn

規則からなる．ここで，メソッドの機能振る舞いは，である. この半順序関係

VDM オペレーションと同様に，事前条件と事後条件

置き換え可能であることを示す. C[ · ]So を So 実行の組で表される．

の文脈とすると, 以下のように書ける．

VDM の証明条件も振る舞いサブタイプ規則も，事

So

Sn ⇔

は，Sn が So の代わりに

C[Sn ]So が可能.

前条件を弱め，事後条件を強めるという考え方にた

すなわち, Sn を So の代わりに用いることで，So のつ．弱い事前条件の規則は，So 起動がエラーを生じ場合に壊されていた性質 ϕ が Sn を用いる場合に満たない実行環境で，Sn も実行時エラーを起こさないとされることを表す．Sn は，外部環境 D の下で ϕ をいう条件を表す．強い事後条件の規則は，Sn は So

満たすという点で，So よりも制限的であると云える．

よりも強い条件を表すことであり，包含する振る舞い
機能を有することを表す．既存のコンポーネント So

4. 2 インテグリティ・ポリシー

よりも詳細な（具体的な）記述を持つことや，機能拡次に，張を可能にすることを目的とした方法である．

の具体的な関係を探す. このような半順序関係を満たす候補は数多くあるが，本論文では，イン

一方，自己適応システムでの置き換え可能性では，

テグリティを用いる．特に，以下に説明する Biba イ

新しく導入したコンポーネント Sn が，不用意に追加

ンテグリティ・モデルのリング・ポリシー ( [1] の第 6

的な機能振る舞いを持たないことを確認したいこと章) を採用する.

がある．このような追加機能が，置き換え前に満たLabel を半順序関係が生成する有限ラティス

されていた制約条件を壊すことを避けたい．たとえを構成するラベルの有限集合とする．また，2 つば，Sn が，追加した機能によって，情報を漏洩するの 特 別 な 要 素 ，トップ ( ) と ボ ト ム (⊥) が あ り,

ような場合，コンフィデンシャリティが壊される．ま∀e ∈ Label . e

た，データベース内容を破壊するような機能追加があユーティリティ関数 max（min）はラベルの有限集∧⊥ e を満たすとする. さらに，

ると，インテグリティが満たされなくなる．したがっ合を引数としてとり，その極大要素（極小要素）を返て，Sn が，So に対して，制限された機能振る舞いにす．つまり，2 項オペレータ join (meet) (たとえばなっていることを確認する方法が必要である.

[5]) を入力引数として有限集合をとるように拡張した関数とする．

4 インテグリティに基づく置き換え可能性あるプログラム（サブジェクト）がオブジェクトを参

本節では、自己適応 Web アプリケーションシステ

照する場合を考える．サブジェクトとオブジェクトは，

インテグリティレベルを表すラベル Lj (Lj ∈ Label)

言語を考える．以下，S は文を，E は式を，B はブーを持つとする. Biba リング・インテグリティ・ポリ

ル式を, P は手続き名（関数名）を，DB は永続デー

シーは以下の規則で表される．

タ領域を各々表す．

(1) サブジェクトは，インテグリティレベルによらS := x = E(assignment)

ずに，どのようなオブジェクトであっても読み出| if B then S1 else S2(conditional statement)

し可能である．

| while B do S

(loop statement)(2) サブジェクト S がオブジェクト O に書き込み可能なのは，LO

LS であり，その時だけである.

(3) あるサブジェクト S1 が他サブジェクト S2 を実行できるのは，LS2LS1 であり，その時だけである.

| call P(E)(procedure call)| S1 ; S2(sequencing)| write(DB)(write access)| read(DB)(read access)

次に，関数 L を，プログラム文 (S) からインテグリ
ティラベル (Label) へのマップ, L : S → Label とBiba インテグリティは規則 (2) と (3) から，下流向

する. L を，先に示した文の構文構造にしたがってき（ﬂow down）規則と呼ぶことがある．

帰納的に定義する．特に，手続き (関数) P の本体

規則 (2) は，サブジェクトが，より重要性の高いオは文 S とすると，プログラム本体 S に，以下の規ブジェクトへの書き込みを禁止する．より重要なオブ則を適用することで，すべての LDB j ラベルの極大

ジェクトを変更可能とすると，誤ったデータを書き込（max({LDB j s})）が得られる.

む可能性を排除できない．規則 (3) は，自身よりも重L[[x = E]] = ⊥要性が低いサブジェクトだけを実行可能とする．これ

L[[if B then S1 else S2]] = max({L[[S1]], L[[S2]]})

によって，信用度の低いサブジェクトが実行制御を握L[[while B do S]] = max({L[[S]]})

るような場合を排除する．

L[[call P (E)]] = LP

2 つのサブジェクト，SS と SW ，が関わる簡単なL[[S1 ; S2]]= max({L[[S1]], L[[S2]]})

例題シナリオを考える．SS は DH と DL の両方に書

L[[write(DB)]] = LDB

き込みアクセスが可能であるが, SW は DL のみとすL[[read(DB)]] = ⊥オブジェクト間のレベルを，LDL ≺ LDH

上記の規則中，手続き（関数）呼び出しの場合，ラと 仮 定 す る. こ の 時, LSW ≺ LSS と な る ．そ の

ベルを LP と表記した．これは，当該手続き（関数）

理由は，LDL ≺ LSW , LDH ≺ LSS , LDL ≺ LDH ,の本体 Sbody に，上記の規則をボトムアップ的に適用る. また,

LDH ≺ LSW が成り立つことである. その結果，SWすることで計算でき，max({L[[ Sbody ]]}) になる. まを，SS の代わりとして使うことができる．つまり，た，再帰的に定義される手続き（関数）では，自身

SW は SS を制限するものであり，実際，SW は DHのラベルを仮に X とする時，X = max({Lj s, X})に書き込み不可である一方, SS は可能である.

を満たすことになる. max({Lj ’s})

X の場合，

X = max({Lj s}) を解に持つ．今，X の最小ラベル
4. 3 サブジェクトのラベル計算に関心があることから, X = max({Lj s}) としておラベル LOj を持つことがわかっている一群のオ

けば良い.

ブジェクトが与えられた時，このオブジェクトすべ

一方，PHP では，文字ストリングデータから実行てに書き込み可能なサブジェクトが満たす最小ラ

時にシンボルを生成し，このシンボルを例えば手続き

ベル LS を計算する手順を考える．以下のように，名として使うことができる．このような場合，実行時

LS = max({LOj s}) を満たすことがわかる.

になってはじめて手続きが決まるので，上記に述べた

ラベル計算法を説明する準備として，データベース

ボトムアップな静的解析だけではラベルを決定する

参照機能を考慮した簡単な手続き型プログラミングことができない，このような場合，実行時に呼ばれる

可能性のある手続きに対して，予め，そのインテグリ

ラムを起動するコマンドとなる†2 . そこで，Web アプ

ティラベル (LP ) を注釈として付与しておく方法が考リケーションを，Web ページ nj が送出する HTTP

えられる．この注釈を用いることで，上記のラベル計

リクエストの列 h0 , h1 , . . .  と考えるほうが良い．

算を簡単化することができる．

ここで，hj はサーバ側プログラムの起動 Pj と 1 対 1に対応し，その列 P0 , P1 , . . .  は，アプリケーショ

4. 4 置き換え可能性検査規則

ン・ユースケースを実現するプログラム実行列に対応

SW を，SS の代わりに用いる置き換え可能性は SS

する．

と SW のラベルに関わる半順序関係で定義する．つ今 ，Web ア プ リ ケ ー ション が 実 現 す る ユ ー ス

LSS の時に，C[SW ]SS が可能になる.

ケースを U (k) と表すと，上記の議論から，U (k) を= L SW

L SS

P0 , P1 , . . .  と同一視できる．そこで，コンポー

ここで，ラベル LSW と LSS は第 4. 3 節の方法で計ネントの場合と同様に考えることで，ユースケース

算する．この計算は, 本質的には，Biba リング・イン

U (k) のインテグリティ・ラベルをサーバ側プログラ

テグリティ・ポリシー規則からなる．

ム Pj

まり，LSW

SS

SW

def

第 3. 1 節に示したシナリオは，次のような関係からなっていた，(a) D, (S, SS ) |= ϕ,


(k)

(k)

(k)

(k)

の最大として定義できる．ここで，Pjのラベルは第 4. 4 節の方法で計算する. したがって，次の関係が成り立つ．

LU (k) = max({LP (k) }).
j(b) D , (S, SS ) |= ϕ,

この関係を用いることで，ユースケース Un を Uo の(c) (S, SS ) ; (S, SW ),代わりとして使う場合の置き換え可能性 Uo(d) D , (S, SW ) |= ϕ.

定義する．

SS

SW であるとは，Biba リング・ポリシーによっ

Uo

def

U n = L Un

Un を

L Uo

て，インテグリティの観点から，SW が SS の制限に

つまり，Web アプリケーションの置き換えは，実現なることである．

するユースケースの変更であり，そのユースケースを実現するプログラム・コンポーネント群の置き換えに

4. 5 Web アプリケーションの置き換え可能性

なる．

Web アプリケーションは複数の Web ページから構成される (たとえば [23]) ことから，置き換え可能

4. 6 実行時情報の利用性について，Web ページ遷移を考慮する必要がある．

インテグリティ・ラベル LS は，ソースプログラム

静的に遷移系列を決めることができる場合，ノードに対する静的解析によって，max({LDB j s}) と計算を Web ページ P age，エッジを関係 P age×P age のされる（第 4. 3 節）．この時，オブジェクトのインテ部分集合とするようなグラフとなる．しかし，Web

グリティ・ラベル LDB j は事前にわかっていることがアプリケーションは，PHP のようなサーバ側スクリ前提となる．しかし，実際に使用されるオブジェクト

プト言語を用いて記述された動的ページを持つので，は，実行時にならないと決まらない場合がある．たと

ページ遷移が静的に決まらない．そこで，Web アプ

えば，PHP プログラムでは，connect コマンド実行

リケーションの利用者からみたユースケース・シナリ

によって，特定のデータベースを接続して使う．このオに対応する Web ページ遷移列の集合と見做す．

オブジェクトのインテグリティ・ラベルが上記の計算

n0 , n1 , . . .  を，動的に生成されたページ nj の列で用いられたラベルと一致するとは限らない．そことする．各ページ nj は複数の HTTP リクエストをで，Web アプリケーションに対しては，ユースケー

Web サーバに送り，その各々が特定のサーバ側プログスの置き換え可能性検査 (UoUn ) に加えて，PHP†2 第 5 節の図 2 に具体例の模式図を示す．

ここで，時相オペレータ 2 (常に) と 3 (いつか) を

HTTP:login
P0
Web Pagen1

用いた．また，HTTP(select) は注文の HTTP リク
PHP Program

エストを受け取った時に論理真となり，HTML(sold)

HTTP:list
P1

は購入完了 GUI ビューを持つ HTML 文書が Web ク

n2

HTTP:selectライアントに戻された時に論理真となる.

P2
n3

実行中に，上記の LTL 式 ϕ が満たされなくなる場
HTTP:connue

合を考察する．在庫管理の主データベース更新につP3
n4

いて 2 つの方法を併用していて，利用者の振る舞い

HTTP:conﬁrm
HTTP:cancel

n5P4が想定と異なる場合に起こる実行干渉が原因である．

P5

n6

この EC サイトが提供するユースケースを実現した

Web ページの遷移列を図 2 に示した．HTTP リクエ
図2

スト login によって PHP プログラム P0 が起動され，Page Transitions

Web ページ n1 に遷移する. 以降，図に示されたようプログラム実行時の検査を併用する必要がある．

な実行列をたどる．この Web ページ遷移列は 2 つの

今， connect コマンドによって使用開始するオブ

更新方式に共通であるが，PHP プログラムの機能振ジェクト insDB j のインテグリティ・ラベルを LinsDB j

る舞いは異なる．プログラムの概要を，図 3 (SEarly )とする．LS を静的な解析によって max({LDB j }) を求と図 4 (SLate ) に模式的に示す. これらは，もとのめた時に使ったラベルとする時，LinsDB j

LDB j を確認できれば良い．実際は，LS は max({LinsDB j }) とPHP プログラムから，データベース参照の列だけを抜き出した．

なるべきである．一方，LinsDB j

LDB j が成り立つ

文献 [20] では，本 EC サイトを実行時に改変することがわかると，max({LinsDB j })max({LDB j })自己適応システムとして実現している．PHP アプリ

LS であり置き換え

ケーションのファイルは，HTTP リクエストに対応である．したがって，LinsDB j
に関して安全なことがわかる．

して Web サーバに動的にロードされる．システムの改変 (S ; S  ) を行うには，PHP プログラムのソー5 適用の事例

スファイルを置き換えるだけで良い．

提案の置き換え可能性を簡単な電子商取引き（EC

次に，PHP プログラムの置き換え可能性検査につサイト）の自己適応 Web アプリケーション [20] に適いて考える．考察対象のプログラムは在庫データベー用する. 具体的な自己適応のシナリオは文献 [20] にあスという永続データを更新していることから，インテ

るが，以下，概要を説明する. 開発時に気付かなかっグリティが大切な観点になる．置き換え後のプログラ

た利用者の振る舞いによって，EC サイト運営者が素

ムは，重要性の高いデータを壊してはならない．

朴に期待する要求性質が壊される．つまり，運営者の自己適応 EC サイトは，先に述べた性質 ϕ が，再高次ゴール [15] あるいはポリシー [6] が満たされない

び満たされるように，自身の機能振る舞いを変更すシナリオを考える．
．

る．以下のシナリオでは，ここでの考察に必要な対象「在庫のある商品の購入希望顧客がいる場合，だけを明示する．D j は利用者の振る舞いを表し，Sx

その顧客に商品を販売する.」がデータベース更新を司るプログラムとする．この

この要求性質は，原子命題をうまく選ぶことで，LTL

EC では，利用者に，プレミア会員と通常会員の 2 つの論理式として表現することができる．具体的には，のサービス・レベルを設けている．EC サイトは，利次のような LTL 式 ϕ となる．

用者ログイン時に，会員クラスに応じて，SEarly あ

def

ϕ = 2(enoughStock ∧ HTTP(select)⇒ 3HTML(sold))

るいは SLate のどちらか一方のプログラムを選択する. 以下のシナリオでは，D  1 が SEarly を，D  2 が----- P1 ---------- P1 -----

select(DB);// read DB

select(DB);----- P2 -----// read DB----- P2 -----

create(TS, y);// write TS

create(TT, y);insert(DB, y);// write DB----- P4 ---------- P4 ----destroy(TS);// write TS----- P5 -----

select(TT);// read TT

select(DB);// read DB

insert(DB, y);// write DB// write TT

select(TS);// read TS

destroy(TT);update(DB,y);// write DB----- P5 -----

destroy(TS);// write TS

destroy(TT);-----// write TT// write TT----図3

Early Mode

図4

SLate に対応する．

Late Mode

第 4 節の方法を，図 2 が示す 2 つのユースケー
今，あるプレミア会員 D 1 が，注文して直ちに取りス（Conf irm と Cancel）に適用する．Conf irm と消すという奇妙な振る舞いを繰り返すとする．また，Cancel は，各々，以下のようなプログラム実行列か

D 2 は通常会員であって，期待通りの購入行動に従うらなる．

とする．この時，D 1 の振る舞いが原因となって, 上Conf irm = P1 , P2 , P3 , P4 ,記の性質 ϕ を満たさないような実行時干渉が起こる

Cancel = P1 , P2 , P3 , P5 .
図 3 を基に，インテグリティ・ラベルを求める．

可能性がある．
LEarlyConf irm = max({⊥, LDB , ⊥, LT S }) = LDB ,(D 1 ||D 2 ), SEarly ||SLate |= ϕ
自己適応 EC サイトは，このような実行時干渉を検知し，再び性質 ϕ が満たされるように，自身のコンLEarlyCancel = max({⊥, LDB , ⊥, LDB }) = LDB .
同様に，図 4 から，以下がわかる．

ポーネントを入れ替える．つまり，プレミア会員 D 1

LLate
Conf irm = max({⊥, LT T , ⊥, LDB }) = LDB ,に対するサービスを実現するプログラムを変更する．

LLate
Cancel = max({⊥, LT T , ⊥, LT T }) = LT T .

(D 1 ||D 2 ), SX ||SLate |= ϕ以上より，購入ユースケース（Conf irm）の場合はしたがって，既存プログラム SEarly を置き換える新LLate = LEarly である一方，キャンセル・ユースケー

しいプログラム SX を決定する．文献 [20] では，SLateス（Cancel）では LLate ≺ LEarly になる．これらを新しいプログラムとした．つまり，SEarly を SLateを組み合わせると，本 Web アプリケーションが提供に置き換えることが安全であるかを検査する問題にするユースケース全体に対して，LLate

なる．

得られる．ユースケースに対するインテグリティ・ラ

次に， SEarly (図 3) と SLate (図 4) が実行する

LEarly がデータベース参照の列を調べる．LDB , を永続デー

ベルの関係は，そのユースケースを実現するプログ
ラムの関係にも当てはめることができる†3 . そこで，

タベース (DB) の，LT S ,LSLateLT T を一時データ領域

LSEarly が成り立ち，SEarly

SLate とな

(TS と TT) のインテグリティ・ラベルとする. また，る．すなわち，C[SLate ]SEarly が表す置き換え関係は永続データベースは一時データ領域よりも重要性が安全なことがわかる。

高いので，LT S ≺ LDB ならびに LT T ≺ LDB が成り立つとする．

†3 文献 [20] は，あるユースケース実現に関わるプログ
ラム群を決定する方法を論じている.

第 4 節の方法は，第 3. 1 節で触れた復帰シナリオ法を提案している．並行コンポーネントシステムのにも適用可能である．上記に述べた機能の置き換え

モデル検査について，反例を用いた述語洗練法 (CE-後，システム作動状況が変化して，D から D に戻GAR) と仮説・確認（assume-guarantee）アルゴリズ

り, その結果，一度，壊れた性質が，再び満たされる

ムを組み合わせる. コンポーネント S の振る舞い仕様

ことがある．上記の具体例では，好ましくない振る

Behv(S) をもとに，So Sn = Behv(So )⊆Behv(Sn )舞いをするプレミア会員がいなくなった状況である．

によって置き換え可能性を定義する. つまり，VDM

def

つまり，すべての利用者が，素朴に期待されるようなのオペレーション・リファインメント [12] や振る舞い

振る舞いを示す場合に戻ったとする．このような時，

サブタイピング [16] と同様に，機能が追加的になるよ

当初の機能を提供するように，再度プログラムを置きうは場合の置き換え可能性を論じている．見かけの不換えるように自己適応 EC サイトを構築しても良い具合を減らすヒューリスティックスのひとつとして，だろう．以下の関係を満たすような SX に置き換える

バグのある振る舞い B を So から除去するアイデアことになる．

が示されている．Behv(So \B) ⊆ Behv(Sn ) と表現(D1 ||D2 ), SX ||SLate |= ϕできる．B を求める方法には触れていない．

元の機能に戻すという選択では，上記の SX は SEarly

本論文では，インテグリティ [1] の考え方を基本になる．これは，SLate に代えて，SEarly に置き換とする置き換え可能性を提案した．これは，デーえることになり，関係 SEarly SLate に違反するよタの重要性という特別な性質に注目したものでうに思える. しかし，文脈 C[ · ]X を用いた考察をあ る ．今 ，B を 置 き 換 え 後 に 除 去 す る 振 る 舞 い

行うと，置き換えが可能であることがわかる．このと す る 時 ，本 論 文 の 置 き 換 え 可 能 性 (So Sn ) を置き換えは，実際には，当初が SEarly 使われていBehv integrity (So \B) = Behv integrity (Sn ) と考えるた文脈に，SEarly を挿入することである．つまり，ことができる．ただし，Behv integrity (S) は，もとのC[SEarly ]SEarly なので，安全なことがわかる．

プログラムからインテグリティに関する側面を保存した振る舞い仕様である．第 4 節は，Behv integrity (S)6 議論

を計算する方法を構成的に与えている.

自己適応システムを適切さ規則 [11] を用いて論じ本論文では，Biba リング・インテグリティ・ポリ

る試みは文献 [9] で採用された. その後，文献 [20] が，シーをもとに，置き換え可能性を定義した．置き換え

モデルベース自己適応アーキテクチャ [8] ならびに実後の新しい Sn が大切なデータベースを不用意に壊さ

行時干渉 [19] との関係を明らかにした．本論文は，こないようにすることが目的であった．第 5 節に紹介の流れの研究であり，文献 [22] のアイデアを，より詳した電子商取引システム（EC サイト）は，在庫デー細化した. 特に，第 4 節で,Web アプリケーションにタを格納する永続データベースと利用者セッションご適用する際の技術的な議論を具体的に行った．

とに一時格納領域を用いている．永続データのほうが文献 [3] は，ソフトウェア工学からみた自己適応シ
ステム研究のロードマップを整理した．5 つの主要課

一時的なデータよりも重要なので，インテグリティが適切な方法であった．

題のひとつして，品質保証の問題が重要であることを一方，第 4 節に示した置き換え可能性の一般的な指摘している．実際，形式手法として研究されてきた定義によると，Biba リング・インテグリティ・ポリ

技術を自己適応システムに応用する試みが多数ある

シー以外の半順序関係を用いた定義でも良いことが[27]．主な研究としては，コンポーネント置き換え前

わかる．たとえば，コンフィデンシャリティが重要な後での振る舞い等価性を考える (たとえば [13]).

安

アプリケーション・システムを対象とする場合であれ

全性，到達性，活性といった一般的な性質を取り扱っ

ば，Bell-LaPadula (BLP) ポリシー [1] を使う等の工ている．

夫をすれば良いだろう．

文献 [2] は，置き換え可能性に関する自動検証の方

7 おわりに
本論文は，自己適応システムでの安全な置き換え可能性の考え方を論じ，ついで，インテグリティに基づく方法が，電子商取引システムの自己適応 Web アプ
リケーションで有用なことを示した．永続データ領域の不用意なデータ破壊を阻止したいからである．この置き換え可能性検査の方法では，開発時に行う静的検査 (第 4. 3 節) だけではなく，実行時検査 (第 4. 6 節)も併用しなければならないことがわかった.
本論文の適用シナリオでは，置き換え可能性の検査を人手で行った．PHP プログラムを対象とした自動検査ツールの開発は今後の課題である．
謝辞 本研究の一部は科学研究費助成事業

学術研

究助成基金補助金挑戦的萌芽研究 23650019 の支援を受けて実施した．

参 考 文 献[ 1 ] M. Bishop. Computer Security, Addison Wesley,
2003.
[ 2 ] S. Chaki, E. Clarke, N. Sharygin, and N.
Sinha. Veriﬁcation of Evolving Software via Component Substitutability Analysis, Form. Methods Syst.
Des., no.32, pp.235-266, 2008.
[ 3 ] B.H.C. Cheng, R. de Lemos, H. Giese, P. Inverardi, and J. Magee. Software Engineering for SelfAdaptive Systems: A Research Roadmap, In SelfAdaptive Systems, pp.1-26, 2009.
[ 4 ] F. Dalpiaz, P. Giorgini, and J. Mylopoulos. An Architecture for Requirements-Driven Selfreconﬁguration, In Proc. CAiSE 2009. pp.246-260,
2009.
[ 5 ] B.A. Davey and H.A. Priestley. Introduction to
Lattices and Order (2ed.), Cambridge University
Press 2002.
[ 6 ] S. Fickas and P. Nagarajan. Critiquing Software Speciﬁcations, IEEE Software, No.11, pp.3747, 1988.
[ 7 ] S. Fickas and M. Feather. Requirements Monitoring in Dynamic Environments, In Proc. RE’95,
pp.140-147, 1995.
[ 8 ] D. Garlan, S.W. Cheng, A.C. Huang, B.
Schmerl, P. Steenkiste. Rainbow : Architecturebased Self-Adaptation with Reusable Infrastructure, Computer, 37(10), pp.46-54, 2004.
[ 9 ] C. Ghezzi. Adaptive Software – the fadingboundary between development time and run time,
An invited Talk at SEAMS 2011, May 2011.
[10] C. Ghezzi, L. S. Pinto, P. Spoletini, and G.
Tamburrelli. Managing Non-functional Uncertainty

via Model-Driven Adaptivity, In Proc. ICSE 2013,
pp.33-42, 2013.
[11] M. Jackson. Requirements & Speciﬁcations,
Addison-Wesley, Reading, 1995.
[12] C. Jones. Systematic Software Development using VDM (2ed.), Prentice Hall, 1990.
[13] N. Khakpour, M. Sirjani, and U. Goltz. Contextbased Behavioral Equivalence of Components in
Self-Adaptive Systems, In Proc. ICFEM 2011,
pp.16-32, 2011.
[14] J. Kephart and D. Chess. The Vision of Autonomic Computing, IEEE Computer, Vol.36, No.1,
pp.41-50, January 2003.
[15] A. van Lamsweerde. Goal-Oriented Requirements Engineering : A Guided Tour, In Proc.
RE’01, pp.249-263, 2001.
[16] B. Liskov and J. Wing. A Behavioral Notion of
Subtyping, ACM TOPLAS, Vol.16, No.6, pp.18111841, 1994.
[17] V.P. La Manna, J. Greenyer, C. Ghezzi, and
C. Brenner. Formalizing Correctness Criteria of Dynamic Updates Derived from Speciﬁcation Changes,
In Proc. SEAMS 2013, pp.63-72, 2013.
[18] B. Morin, O. Barais, J.-M. Jezequel, F. Fleurey,
and, A. Solberg. Models@run.time to support dynamic adaptation. IEEE Computer, Vol.42, No.10,
pp.44-51, October 2009[19] S. Nakajima. Detecting Feature Interferences in
PHP-based Web Applications, In Proc. 22nd ICSSEA (CD-ROM edition), 2010.
[20] 中島震. 自己適応 Web アプリケーション，コンピュー
タソフトウェア，vol.29, No.3, 54-69, 2012.
[21] 中島震. 実行時干渉の発生確率予測，コンピュータ
ソフトウェア，2013.
[22] S. Nakajima. Safe Substitution for Servce-based
Applications, In Proc. QASBA’13, 2013.
[23] F. Ricca and P. Tonella. Analysis and Testing of
Web Applications, In Proc. 23rd ICSE, pp. 25-34,
May 2001.
[24] W. Robinson and S. Purao. Specifying and Monitoring Interactions and Commitments in OpenBusiness Processes, IEEE Software, pp.72-79,
March/April 2009.
[25] D. Sykes, D. Corapi, J. Magee, J. Kramer, A.
Russo, and K. Inoue. Learning Revised Models forPlanning in Adaptive Systems, In Proc. ICSE 2013,
pp.63-71, 2013.
[26] Y. Wang, S.A. McIlraith, Y. Yu, and J. Mylopoulos. An Automated Approach to Monitoringand Diagnosing Requirements, In Proc. ASE 2007,
pp.293-302, 2007.
[27] D. Weyns, M.U. Iftikhar, D.G. de la Iglesia, andT. Ahmad. A Survey of Formal Methods in SelfAdaptive Systems, In Proc. C3S2E-12, pp.67-79,
2012.
[28] J. Zhang and B.H. Cheng. Model-Based Development of Dynamically Adaptive Software, In Proc.
ICSE’06, pp.371-380, 2006.