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

確率的プログラムの AOP による生成中村 隼也

渡辺 啓介

佐藤 亮介

鵜林 尚靖

亀井 靖高

ソフトウェア工学において，不確かさを包容したソフトウェア開発は重要な研究課題の 1 つである．本論文では，Known-Unknowns（既知の未知）を記述することのできるインターフェース機構 Archface-U に確率を導入し，以下を可能とする: 1) 確率的な振る舞いをインターフェースとして記述; 2) インターフェースレベルで確率的モデル検査を実行; 3) 仕様としてのインターフェースからコードへのリファイメントをプログラム変換により実現（確率を含まないコードをインターフェース記述を元に確率を考慮したコードに自動変換）．これにより，モデル検査によって動作保証された確率的プログラムの開発が容易となる．などが挙げられる．また，Amine M. らは Event-B [1]1 はじめにの非決定性を確率的な選択で置き換えた Probabilistic

ソフトウェア開発の様々な工程で発生する「不確かEven-B を提案している [4]．

さ」に我々は対処していかなければならない．
「不確

しかし，確率を考慮したプログラムを作成し，コーかさ」には，その不確かさの存在に誰も気が付いていドレベルで振る舞いの正しさを検証することは難しない状態である「未知の未知」と，その不確かさの存い．その例として，コードレベルでのモデル検査には在に気が付いているがどう対処していいかがわから状態爆発の問題があることが挙げられる．このようなない「既知の未知」の 2 つの種類がある．
「未知の未問題に対処するために，不確かさを記述することので知」に対処することは現状では難しく，ここでは後者

きるインターフェース機構 Archface-U [5] が確率的なの「既知の未知」に焦点を当てて，以降の不確かさは不確かさを記述できるように拡張し，インターフェー全て「既知の未知」とする．

スレベルでモデル検査を行うことで振る舞いの正しさ不確かさの性質の 1 つに確率的な不確かさがある．

を検証する手法を提案する．この手法により，モデルこれは，システムや環境が確率的な振る舞いをするこ検査を行う対象がインターフェースになることでコーとなどにより発生する不確かさである．近年確率的なドレベルのモデル検査より状態爆発する可能性が小さ挙動で表される不確かさを扱うことのできる言語やくなる．そして，インターフェースのモデル検査によツールが注目されている．その例として確率的プログり保証された性質は，インターフェースに従って実装

ラミングや確率的モデル検査器 PRISM [6] や PAT [8]されているコードに対しても保証されるため，コード

Probabilistic Programming by AOP.
Shunya Nakamura, Keisuke Watanabe, 九州大学大学
院システム情報科学府, Graduate School and Facultyof Information Science and Electrical Engineering,
Kyushu University.
Ryosuke Sato, Naoyasu Ubayashi, Yasutaka Kamei,
九州大学大学院システム情報科学研究院, Graduate
School and Faculty of Information Science and Electrical Engineering, Kyushu University.の動作を保証した確率的プログラムの開発が容易になる．本論文では確率的な不確かさをインターフェースに記述し，それを元に確率的プログラミングを生成する手法について述べる．具体的には，Archface-U レベルで確率的モデル検査を行い，振る舞いの正しさが保障されれば，Archface-U に記述された確率を元に，確率を含まないプログラムコードから確率を含むプログラムコードへと自動変換する．本論文では，2 章で関連研究について述べる．3 章では不確かさを包容したインターフェース機構 Archface-U を紹介する．4 章では Archface-U の型検査と確率モデル検査による振る舞いの検証について述べる．5 章で確率的プログラムの生成について述べ，6 章ではまとめと今

01: interface component Main {02:

void actionPerformed(ActionEvent e);

03: }
04:
05: interface component StudentController {06:

void filterStudent(JTable table);07:

void colorStudent(JTable table);08: }09:

後の研究の課題について述べる．

10: interface connector cStudent {}11:2 関連研究12: uncertain connector ucStudent extends cStudent {2. 1 確率的モデル検査器 LTSA-PCA

14:{StudentController.filterStudent,

15:

StudentController.colorStudent} -> Main);13:

Student = (Main.actionPerformed ->モデル検査とは，検査対象のシステムの振る舞い

16: }が，検査したい性質 (プロパティ) を満たすかどう

図1

e ラーニングシステムにおける Archface-U の記述かを判定するものである．LTSA-PCA [9] は確率的振る舞いをするシステムを扱えるようにモデル検査

象モデルに対する正当性を保証する．Probabilistic器 LTSA(Labelled Transition System Analyser) [7]

Event-B [4] は Event-B の全ての非決定的な選択を確を拡張したものである．LTSA-PCA においてモデ率的な選択に置き換えたものである．Event-B の非決

ルの記述は Probabilistic FSP(Finite State Process)

定的な選択は，実行可能なイベントの選択，パラメーという記法を用い，これは LTSA でモデルを記述す

タ値の選択，非決定的な割り当ての 3 つであり，それるための記法である FSP を確率が表現できるようぞれに対して重みの付与や離散分布などによって非に拡張したものである．LTSA-PCA は Probabilistic

決定的選択を確率的選択に置き換える．Probabilistic

Component Automata（PCA) [10] としてモデル化

Event-B はリファインメントをする際に Event-B のされたコンポーネントベースのシステムの確率的な振通常の証明責務に加えて，確率に関する証明責務も証る舞いをグラフィカルに表示する機能や，システムの明する必要がある．現時点では実行可能なコードを故障解析などの機能を有する．モデル検査器 PRISM

生成する直前のリファインメントにおいてのみ確率はマルコフ連鎖 (DTMC) を状態遷移系として扱い，を与えることが可能であり，それ以前のリファインメモデルが検査したい性質を満たす確率を求めること

ントは非決定的選択は確率に置き換えることができができる [6]．LTSA-PCA でシステムが故障する確率ない．確率的な振る舞いをするシステムを対象にしなどを求める場合は，PCA を DTMC に自動的に変ている点では本手法と一致しているが，Probabilistic換し，PRISM のようなツールを用いて計算する．本

Event-B は仕様と確率付きプログラムを作成しなけ

研究では確率を記述したインターフェースのモデルればならないが，本手法では確率を記述したインター検査のために LTSA-PCA を利用する．これは，インフェースとプログラムコードがあれば自動で確率付きターフェースでのメソッドの振る舞いは，LTSA でモプログラムコードを生成できるという点で異なる．

デルを表現するための記法である FSP(Finite StateProcess) に準拠した文法で記述するためである．

3 不確かさを包容するインターフェース機構
Archface-U

2. 2 Probabilistic Event-B
Event-B [1] は要求仕様から段階的にリファインメントを行うことで，詳細なモデルを構成していく手法である．リファインメント毎にそのリファインメントに対する証明責務を証明することによって，抽

本章では不確かさを記述可能なインターフェース機
構 Archface-U について説明する．

3. 1 Archface-U

filterStudent と colorStudent のどちらが呼び出され

Archface-U は，アーキテクチャ設計と実装間の不るかが不確かであることを示している．Alternative

一致を無くすためのインターフェース機構である．

な不確かさの場合は，少なくともどれか 1 つが実装

Archface-U はプログラム全体の制約を記述することされていなければ型検査によりコンパイルエラーとのできるインターフェースであり，Archface-U に記なる．Optional な不確かさの場合は，Optional の性述された内容を実装することを強制する．Archface-U

質ゆえにそのメソッドを実装しても実装してなくてもは不確かさを記述することが可能であり，図 1 にそ型検査でコンパイルエラーにはならない．の記述例を示す．この例は，ある大学で用いる e ラー
ニングシステムにおける受講者一覧機能を記述した

3. 2 重みによる確率記述ものである．いま，受講者のみを一覧表示すべきか，これまでの不確かさの記述は，不確かなメソッドそれとも全学生をリスト表示した上で受講者のみをが存在していることを示すものであり，実際に呼び出色付表示すべきかが決定できない状況を想定して欲される，または実装されるメソッドはいずれ開発者しい．すなわち，どちらの表示方式を採用すべきか判によって決まるものであった．以降は不確かなメソッ断できないという不確かさが存在する．

ドが確率によって振る舞いが振り分けられる，すなわArchface-U は Component-and-Connector アーキ
テクチャ [3] に基づいており，Component と Connec-

ち，設定された確率に従って呼び出されるメソッドが変化する状況についても考える．

tor の 2 つのインターフェースからなる．Component

Archface-U では，不確かなメソッドが実行されるインターフェースは Java のインターフェースと同様確率を重みによって表現する [12]．図 1 の e ラーニのものであり，実装しなければならないクラスと，そングシステムの例では，受講している生徒の一覧をのクラスが持たなければならないメソッドを型，引表示する 2 つのメソッド候補 filterStudent および数を含めて定義する．図 1 の例では，Main クラスはcolorStudent に対しては Alternative，すなわち，どactionPerformed メソッドを，StudentController ク

ちらを最終的に採用するか分からないという不確かラスは filterStudent メソッドと colorStudent メソッさが存在していることを表している．

ドを実装しなければならないという制約を記述して複数の実装案を比較評価するために，ユーザ毎にそある．また，Connector インターフェースでは，FSPれぞれの実装案を一定の確率に従って切り替えることに準拠した構文で Component 間のインタラクション

で，ユーザの好みや傾向等を統計的に検証する手法を（メソッド呼び出し関係）を記述する．不確かさはキー

A/B テストという [2]．図 1 の 2 つの Alternative なメ

ワード uncertain で定義することができる．uncertain

ソッドで A/B テストを実施することで，どちらの実Component や uncertain Connector は，不確かさを装の方がより使いやすいかをテストすることを考える．

含まない Component インターフェースや Connector

テストを行うため開発者は両方のメソッドを作成し，インターフェースのサブインターフェースであり，記それぞれのメソッドに重み w1 ，w2 (正の有理数) を設述することのできる不確かさは以下の 2 種類である．

定する．重みを設定したことで，actionPerformed の(1) 複数の実装の候補があるが，どの候補を採用する

実行後に filterStudent，または colorStudent が呼びかが分からない．

1
出された場合，確率 w1w+w
で filterStudent の処理
2(2) ある実装について，それを採用するか否かが分か2が，確率 w1w+w
で colorStudent の処理が選択され実2らない．

行される．Optional な不確かさの場合は，当該のメ

前者は Alternative と呼び，複数のメソッドの候補をソッド m と空の処理 ϕ の Alternative とみなし，重{} で囲んで記述する．後者は Optional と呼び，メみ wm ，wϕ を設定する．

ソッドを [ ] で囲んで記述する．したがって，図 1 の重みの設定は，Archface-U に対するアノテーショ

uncertain Connector では actionPerformed においてンを用いる．表 2 に示した 4 種類のアノテーション

表1

インターフェー

可変性の種

スの種類類

uncertain com-

重みと振り分けの確率記述

重み

任意の m の実行時の処理

alternative{m1 , m2 , ...}

w1 , w2 , ...

wk /optional[m1 ]

w1 , w ϕ

w1
w1 +wϕ∑i wi の確率で mk を実行

ponentuncertain com-alternative

nectoruncertain con-ϕの確率で空の処理を実行

ponentuncertain con-wϕの確率で m1 を実行， w1 +w

optionall -> {m1 , m2 , ...}-> n

m1 , m2 , ... もし m が l 中で呼び出されたならば∑wk / i wi の確率で mk を実行

l -> [m1 ] -> n

w1 , w ϕ

もし m が l 中で呼び出されたならば
wϕw1の確率で m を実行， w1 +wのw1 +wϕϕ

nector

確率で空の処理を実行
表2

重みを設定するアノテーション

アノテーション

重みの設定@ExecForce

可変性において挙げられているメソッドの中で，このアノテーションが指定されたメソッドには重み 1 を，それ以外には重み 0 を設定する．

@ExecIgnore

可変性において挙げられているメソッドの中で，このアノテーションが指定されたメソッドには重み 0 を，それ以外には重み 1 を設定する．

@ExecRatio(double p)

このアノテーションが指定されたメソッドに重み p を設定する．また，可変性においてこのアノテーションが指定されている全てのメソッドの p の合計が psum ，指定されていないメソッドの個数が n であるとき，1 − psum > 0 ならば指定されていないメソッド全てに重み 1 − psum を，1 − psum ≤ 0 ならば重み 0 を設定する．

@ExecWeight(double w)

このアノテーションが指定されたメソッドに重み w を設定する．可変性においてこのアノテーションが指定されていないメソッドがあれば重み 0 を設定する．

を使い分けることで，開発者は単に重みを記述するだけではなく，振り分けの割合を直感的に設定したり把握したりすることが可能になる．これらのアノテーションは実行時の振る舞いに影響を与えるため，

Exec アノテーションと呼ぶ．Exec アノテーションは，Archface-U の Component インターフェースのメソッ

01: interface component StudentController {02:@ExecWeight(5)03:void filterStudent(JTable table);04:@ExecWeight(1)05:void colorStudent(JTable table);
06: }
図2

e ラーニングシステムにおける Archface-U のアノテーションの記述 (図 1 からの変更箇所抜粋)

ドに対して記述する．Connector インターフェースの重みの設定は実装上の問題でまだ実現しておらず，今間接的に設定できるようにしている．前述の e ラーニ

後サポートしていく予定である．そのため，現時点でングシステムの例でアノテーションを指定すると図 2は Connector インターフェースに記述されたメソッのようになる．この場合は filterStudent に重み 5 を，ドの振る舞いの確率は，Component インターフェー

colorStudent に重み 1 を設定したことになる．

スで各メソッドに付与された重みを参照することで，フェースに記述されたメソッドの確率は，Connector

4 型検査と確率モデル検査による振る舞い検証

インターフェースに記述されたメソッド振る舞いにおいても反映される．この確率付きの Connector イン

まず，現在リリースしている統合開発環境 iArch-U

ターフェースの記述を Probabilistic FSP(P-FSP) に[11]（確率を含まない Archface-U をサポート）につ変換することで LTSA-PCA による検証が可能にないて述べ，その後，確率を含む場合の検証について述る．LTSA-PCA の検証によりあるプロパティが満たべる．

される確率が計算され，計算結果が好ましくなかった
場合は，開発者は設計の見直しを行うなどして開発を4. 1 iArch-U進めていく．

iArch-U は Archface-U を用いた開発を支援する統合開発環境であり，不確かさを含む UML モデリン

5 確率的プログラムの生成

グ，不確かさのマネジメント，Java プログラミング，Archface-U を仕様とみなすと，プログラムコードおよび検証やテスト等の機能を提供する．型検査はへのリファイメントはウィービングによって自動化でiArch-U のコンパイラにより行われる．型検査では，きる．ここでは，AspectJ による実装方法について説

Arcface-U で記述された振る舞いと Java コードの振明する．

る舞いにシミュレーション関係があるか否かを検査

図 2 の Archface-U の記述に対して生成されるアスする．シミュレーション関係が無い場合はコンパイペクトは図 3 のようになる．図 3 の 4 行目から 9 行

ルエラーとなり，開発者は Archface-U の記述通りに目までは処理が置き換わる条件が記述してあり，このJava コードが実装されるように修正しなければなら条件に合致するとき，元の処理は実行されず 13 行目ない．また，型検査だけでなく振る舞いの検証の機能から 21 行目までの処理に置き換わることになる．こもあり，Archface-U の Connector の記述を FSP にの例では，filterStudent メソッドが actionPerformed変換し，LTSA によりモデル検査を行う．もし，モデメソッドにおいて呼び出されることが条件であり，こル検査で問題が発生しなかったら，型検査をパスしの条件に合致するとき，元々実行されるはずだった

た Java コードの振る舞いも Archface-U の観点ではfilterStudent メソッドの処理は実行されず，代わりに保証される．コードレベルでモデル検査するのではな

13 行目から 21 行目までの処理が実行されることにな

くインターフェースレベルでモデル検査することで，る．colorStudent メソッドについても同様なアスペク状態爆発の問題は緩和される．

トが自動生成される．

13 行目の weightSwitch は，n 番目の引数が an ，引4. 2 確率を含む場合の検証数の和が asum であるとき，an /asum の確率で n を

Archface-U で確率を扱えるように拡張するにあた返すメソッドである．引数は Archface-U のアノテー

り，モデル検査器として LTSA を確率が扱えるようにションで設定した重みであり，ここでは filterStudent，拡張した LTSA-PCA を利用する．また，Java コード

colorStudent のそれぞれに設定した重みが引数となっでは確率を扱える構文を持たないため，Archfacre-Uている．つまり，13 行目の処理では設定された重みの記述からアスペクトを自動で生成し，それを Javaの比に従って，複数のメソッド候補のうち 1 つを確率コードとウィービングする．これにより，確率に基づい的に選択することになる．Optional の場合は，当該て，メソッド実行の振り分けを行うことが可能となっメソッドか空のメソッドのどちらかを確率に従って選た．Archface-U に記述された確率的な振る舞いを持択する処理になる．

つコードが自動で生成されるため，もし，LTSA-PCA最後に，確率的に選択されたメソッドが呼び出さで正しさが保証されていれば，生成されたコードの振れることで一連の振り分け処理が完了する．15 行る舞いの正しさも保証される．Component インター目は filterStudent メソッドが選択された処理であり，

01: @Aspect
02: public class U {03:@Around("call(void com.example.student.StudentController.filterStudent(JTable)) &&04:

args(table) && !cflow(adviceexecution()) &&

05:
06:

withincode(void com.example.student.Main.actionPerformed(ActionEvent))")public Object aroundWeightFilter(ProceedingJoinPoint __pjp, JTable table)

07:

throws Throwable {08:

switch (weightSwitch(5, 1)) {09:

case 0: return __pjp.proceed();10:case 1: com.example.student.StudentController.colorStudent(table); return null;

11:}

12:

throw new IllegalStateException();

13:}

14: }
図3

図4

確率を導入するためのアスペクトのコード

確率プログラムの自動生成の流れ

これは元々の振る舞いと同じである．17 行目は col-

図5

リファインメント

orStudent メソッドが選択された処理であり，これは元々の振る舞いとは別の処理に置き換わることを表である．

す．以上の一連の流れを通すことで，重みを設定したインターフェースおよびプログラムのメタ変数とArchface-U を元に確率に従って処理が置き換わるプロして，s および p をそれぞれ用いる．あるインターグラムを自動で生成することができる．weightSwitch

フェース s に対して，プログラム p がそのインターメソッド内では java.util.Random クラスにより取得

フェースを満たすことを |= p : s と書く．この表記をした疑似乱数を用いるが，乱数ジェネレータのシード用いると，本手法の枠組みは次のように述べることが値，および乱数ジェネレータを振り分けの度に初期化できる．本手法は，|= p : s となる s，p が与えられたするかどうかを設定することができる．

とき，s に確率を付与したインターフェース s′ に対して，|= p′ : s′ を満たすプログラム p′ を AOP によ5. 1 プログラム生成の正しさり自動生成する手法である．このとき，s′ の正しさ

本節では，本手法の正しさを示す準備として，部分をモデル検査によって確かめられれば，自動生成されインターフェース関係やプログラムの模倣関係の表記たプログラム p′ の正しさを確かめられたこととなる．

を導入し，本手法の正しさを表す命題を述べる．これ

本手法に関する形式的な定義が正しく与えられたらの形式的な定義，および，命題の証明は今後の課題

場合，証明すべき命題は次の通りである．

命題 1 任意のプログラム p，p′ ，および，インター′′

容した統合開発環境 iArch-U にて確率的モデル検査

フェース s，s に対して，s が s に確率を付与したもの機能と AspectJ を用いた確率的プログラミングののであり，かつ，|= p : s，p′ = Gen(s′ , p) が成り立自動生成の実装を行っていくことが挙げられる．特′′つのであれば，|= p : s が成り立つ．
′に Connector インターフェース上で重みを設定でき

ここで，Gen(s , p) は本手法により自動生成されるるようにすることで，より正確に確率的な振る舞いプログラムである．

を表現することができる．また，確率の取り扱いやリ以降では，この命題の予想される証明の概略を述

ファイメント等について形式的に記述，および証明をべる．まず，⊢ p : s′ ⇝ p′ という型に基づく変換関することで，本手法の正しさを検証していかなければ係を定義する．これは直観的には，プログラム p がならない．

′′s を満たすようなプログラム p に変換可能という意′味である．このとき，p および s が与えられた場合，′′謝辞 本研究は, 文部科学省科学研究補助費基盤研
究 (A)(課題番号 26240007) による助成を受けた.

′⊢ p : s ⇝ p となる p が唯一つとなるように定義し，そのような p′ を Gen(s′ , p) と定義する．ここで，イ参 考 文 献

ンターフェース上の関数 ProbToNondet(−) を引[ 1 ] Abrial, J.-R.: Modeling in Event-B: System andSoftware Engineering, Cambridge University Press,
New York, NY, USA, 1st edition, 2010.
[ 2 ] Adams, B. and McIntosh, S.: Modern Release Engineering in a Nutshell – Why Researchers
Should Care, 2016 IEEE 23rd International Conference on Software Analysis, Evolution, andReengineering (SANER), Vol. 5, March 2016,
pp. 78–90.
[ 3 ] Allen, R. and Garlan, D.: Formalizing Architectural Connection, Proceedings of the 16th International Conference on Software Engineering,
ICSE ’94, Los Alamitos, CA, USA, IEEE Computer Society Press, 1994, pp. 71–80.
[ 4 ] Amine, M., Delahaye, B., and Lanoix, A.:
Moving from Event-B to Probabilistic Event-B,
Proceedings of the Symposium on Applied Computing, SAC ’17, New York, NY, USA, ACM, 2017,pp. 1348–1355.
[ 5 ] Fukamachi, T., Ubayashi, N., Hosoai, S., andKamei, Y.: Modularity for Uncertainty, Proceedings of the Seventh International Workshop on
Modeling in Software Engineering, MiSE ’15, Piscataway, NJ, USA, IEEE Press, 2015, pp. 7–12.
[ 6 ] Hinton, A., Kwiatkowska, M., Norman, G.,
and Parker, D.: PRISM: A Tool for Automatic
Verification of Probabilistic Systems, Springer
Berlin Heidelberg, 2006, pp. 441–444.
[ 7 ] Magee, J. and Kramer, J.: Concurrency: State
Models &Amp; Java Programs, John Wiley & Sons,
Inc., New York, NY, USA, 1999.
[ 8 ] National University of Singapore: PAT : Process analysys toolkit, http://pat.comp.nus.edu.sg/.
[ 9 ] Rodrigues, P., Lupu, E., and Kramer, J.:
LTSA-PCA: Tool Support for Compositional Reliability Analysis, Companion Proceedings of the36th International Conference on Software Engineering, ICSE Companion 2014, New York, NY,USA, ACM, 2014, pp. 548–551.

数中の確率に関する操作を非決定性の操作に置き換えるものと定義すると，命題 1 は次の命題の系となる．
命題 2 プログラム p,p′ およびインターフェース s，s′ に対して，次を仮定する．
• |= p : s．
• ⊢ p : s′ ⇝ p′ ．
• s = ProbToNondet(s′ )．
このとき，次が成り立つ．

|= p′ : s′′

この命題は ⊢ p : s ⇝ p′ の導出に関する帰納法によって示すことができると予想する．

6 まとめと今後の課題
本論文では，Archface-U に基づいた確率的プログラムの自動生成について述べた．確率をインターフェースに記述することにより，状態爆発を緩和した確率的プログラムのモデル検査が可能となった．これは，インターフェースレベルで確率的モデル検査を行うことで，インターフェースに従って実装されている確率的プログラムにも検査結果が成り立つことによって実現した．また，仕様としてのインターフェース記述からプログラムコードへのリファイメントの自動化などが可能となった．これは，確率を記述したインターフェースからアスペクトを自動で生成し，プログラムコードへウィービングすることによって可能となった．今後の課題として，ツールの面では不確かさを包[10] Rodrigues, P., Lupu, E., and Kramer, J.:
Compositional Reliability Analysis for Probabilistic
Component Automata, Proceedings of the SeventhInternational Workshop on Modeling in Software
Engineering, MiSE ’15, Piscataway, NJ, USA,IEEE Press, 2015, pp. 19–24.
[11] Watanabe, K., Ubayashi, N., Fukamachi, T.,
Nakamura, S., Muraoka, H., and Kamei, Y.:iArch-U: Interface-Centric Integrated UncertaintyAware Development Environment, 2017 IEEE/ACM
9th International Workshop on Modelling in Software Engineering (MiSE), May 2017, pp. 40–46.
[12] 渡辺啓介, 深町拓也, 鵜林尚靖, 細合晋太郎, 亀井靖高: 宣言的な可変性記述による A/B テストの自動化[FOSE2016 推薦レター論文], 日本ソフトウェア科学会
誌コンピュータソフトウェア, 2017.