netail.net

_ [hyCalendar]0.7.8 リリース ▲

ドキュメント書き終えたので hyCalendar 0.7.8 リリース．ふー．

今回は，１日の予定をクリップボードにコピーするのと，TODOリストをコピーする機能だけ．ちょっとメニュー項目の名前は微妙だが．

_ ▲ この機能，きちんと mailto と組み合わせられるようにすれば[この日の予定をメールで送信]みたいなメニューも作れないことはない．

_ [hyCalendar]クリップボード機能強化 ▲

hyCalendar の新機能を実装．TODOリスト，日付に表示される予定（日付メモ＋期間予定＋...）をそれぞれクリップボードにコピーできるようになった．

メールなどで予定を他の人に見せたい人向け．というわけで，またマニュアル書きの仕事が発生．

_ [お出かけ]花菖蒲 ▲

大阪は城北（しろきた）公園の花ショウブが満開だというので人を誘って見に行く．さすがに曇り〜雨だったので公園は閑散としていたが，菖蒲園のほうはにぎやか．主に年配の人が中心．10〜20代っぽい人はまったく見かけず．

様々な品種がずらりと並んでいる様子はけっこう面白い．花の写真は，三脚など機材をちゃんと持ってきて撮影している方々がいる．web上でも検索したらすぐに見つかるみたい．

_ ▲ 帰りに，デザートバイキングのSweetsParadiseという店で昼食兼おやつを食べる．90分で1260円（ドリンクバー付き）．パスタ，スープなど軽食系と，ケーキ類各種．味もそこそこ．梅田から泉の広場に行く途中（富国生命ビル）だったので今まで存在に気づいてなかったのだけど．１時頃だったので少し待っただけで入れたが，２時過ぎた辺りからだいぶ行列が伸びていた．こちらは，狙っていかない限り，少し厳しいかも．

_ 炊飯ジャー ▲

煮物も作れる炊飯ジャーというヘッドラインに惹かれて見てみた．http://nikkeibp.jp/wcs/leaf/CID/onair/jp/mech/313078

煮物作ってるとご飯が炊けないと思うのだけど．

_ [論文] 動的スライス＋プログラムの逆実行 ▲

ICSE 2004 Technical Papers, Slicing より．

Tankut Akgul, Vincent J. Mooney III, and Santosh Pande:A Fast Assembly Level Reverse Execution Method via Dynamic Slicing.Proceedings of ICSE 2004, pp.522-531.

Reverse Execution (逆実行) というのは，プログラムを前の状態に戻すように実行していく手法．普通にやると，途中で捨てられていく情報を保存しておかないといけないので，激しくメモリを消費する．そこで，動的スライスを使って，注目してる部分に関連したところだけが回復すればいい，と割り切った手法．

命令の逆転についても，全部の状態を保存していくのではなく，命令列に対して逆命令列を生成する方法を用いるので，各時点でのレジスタ値を保存する方法よりは経済的になっている．

逆実行がどのくらい役立つかは Agrawal か誰かが研究してたような気がする．特定の値だけ復帰させて，もう一度そこだけ細かく実行して，とかできると，かなり面白いデバッグ作業は展開できる気はする．一度ブレークポイントで止めて「システムの状態を保存」とか指示するのと，後から「戻ってみよう」というのとで，どのくらい開発効率が違うのかは分からないが．

_ [論文] 動的スライス用の実行履歴圧縮 ▲

ICSE 2004 Technical Papers, Slicing より．

Tao Wang, Abhik Roychoudhury:Using Compressed Bytecode Traces for Slicing Java Programs.Proceedings of ICSE 2004, pp.512-521.

Java バイトコードの実行履歴を，RLESe とかいう文から文法を構成するタイプのアルゴリズムで圧縮して，圧縮した状態でも実はそのままスライス計算ができますよーという論文．

動的スライスはコストさえ何とかすれば使える，というふうにみんな考えているのだろうか．静的スライスに比べて研究が活発な気がする．

_ [論文] 動的スライスのメモリ節約 ▲

ICSE 2004 Technical Papers, Slicing より．

Xiangyu Zhang, Rajiv Gupta, Youtao Zhang:Efficient Forward Computation of Dynamic SlicingUsing Reduced Ordered Binary Decision Diagrams.Proceedings of ICSE 2004, pp.502-511.

動的スライスの Forward Computation （１ステップ進むごとに，その時点でのスライスを計算して蓄積していく手法）を使うとき，メモリ消費量を抑える方法の提案．

Binary Decision Diagrams は各ノードが０と１のエッジ（２本だけ）を持っていて末端ノードが０または１でラベル付けされている．で，プログラムスライスはスライスに含まれるIDの集合なので，開始頂点から，IDを表現する２進数（0110とか）で表現されるパスをたどっていくと，末端が０か１かでそのIDがスライスに含まれているかいないか分かる．

で，この論文では，reduced-ordered BDD という，途中のノードをできるだけ共有・省略した状態にすることで各スライスの中身を共有して，全体のデータ量を減らしている．すべてのスライスを合計すると200GB相当のデータになるところが400MB程度で収まるとか．

加えて，スライス基点情報の圧縮とかも何かやっているらしい．（これは去年のICSEで発表されたものっぽい）

プログラムの実行時間については，一番大きい材料（67000LOCくらい）で５時間くらい．一度計算してしまえば好きなだけ動的スライスを取得できるのでおいしいといえるか？

個人的には，ちょっと修正→再実行→スライス計算みたいなやり方で使いたいのであまりうれしくないのだが，空間コスト的には非実用ではなくなった分についてはすごい．CPUがさらに高速化すれば本気で実用になってしまうかも？

_ [OUCC] IRC ▲

IRCに奈良先からのお客様が来る（所属的にはM1の人）．ロボ作り（主に機械学習と画像認識）に協力してくれませんか，という話がメイン．（OUCCの）掲示板に書いておいたけど見てくれた？ということでIRCにわざわざ来てくださったらしい．行動力はあるかも．

組み込み系の敷居は高く感じてるんでは，とか阪大にはソフト屋さんが多いから，とか言ったら，メカ系は自分たちでやるよ，阪大の情報よりすごい人多いから，と色々言われた．

丁寧な口調は最初の概要説明くらいまでで，この辺から対等な口調に移っていたのだけれど，１年〜３年生が話し相手だと思ってるのか，年上の社会人相手でも対等でいいと思ってるのかは謎．M1以上も半分くらいいるのになぁ……．

で，なぜか研究室が金持ち，という話になってしまって，4000万のロボットを作ってる人たちと一緒に仕事してる，先生が世界的に有名だ，と自慢された．そして，COEが取れないから阪大は駄目，COE取れないところは興味なし，といったことを言われた．

あと，聞いた話といえば，卒論の枚数が100枚超えたとか．ソフトウェア工学系のＤ論並み．ロボット関係の研究室らしいので，必須のデータがそれだけある分野なのか，読ませる気がないだけか，情報をまとめる力がないのか，いずれなのかは分からずじまい．その人の先輩には１５０枚書いた人がいたようで，「論文書いてたら１５０枚の偉さがわかるよ」と言われた．残念ながら分からない．

結局，本来の話題（どんなことしているか，など）はほとんどなくて，その挙句に話がそれて，なし崩し状態のままで帰られてしまったのだが，会話の論理が飛躍しまくりで，とても楽しい人だった．

_ [ツール] Eclipse 3.0RC1 ▲

研究室関連のプログラム書く環境用に新しい Eclipse を使ってみようかな？と思ってダウンロードサイトに行ったら，いつの間にやら 3.0RC1 が出現していた．

Java2 SDK 1.5 環境まであと少し？

_ [論文] Ontologyの検査？ ▲

ICSE 2004 Tutorial の概要から発見．

Jin Song Dong:Software Modeling Techniques and the Semantic Web.Proceedings of ICSE 2004, pp.724-725.

Semantic Web の Ontology の関係は複雑だから，UML できちんとモデル化したり，形式仕様記述言語でチェックしたりすると便利だなーという話みたい．あと，形式仕様記述から Ontology を生成するとかいう研究もあるらしい．

どんな場面で役に立つのかよくわからないが，いちおう見てしまったのでメモしとく．

_ [日記CGI] キーワード機能追加 ▲

いーかげん見出しが内容を表現してないので，このCGIにキーワード機能追加．実データとしては，ファイルに keyword タグが追加された．まだキーワードをクリックしたら単なる検索が走るだけだが，そのうちキーワードを含んだデータだけが表示されるようになる予定．（まだキーワードが設定されてないデータのほうが多いのでしばらくは移行せず）

_ [論文] 動的影響波及解析の比較 ▲

ICSE 2004 Technical Papers, Dynamic Analysis より．

Alessandro Orso, Taweesup Apiwattanapong, James Law,Gregg Rothermel, Mary Jean Harrold:An Empirical Comparison of Dynamic Impact Analysis Algorithms.

Proceedings of ICSE 2004, pp.491-500.

実行時にデータを集めるタイプの影響波及解析のうち，メソッドの呼び出し関係をきちんと意識する PathImpact とその実行履歴で呼ばれたか呼ばれてないかだけを情報として使うCoverageImpact の実験的な比較．

PathImpact は実行履歴が大きくなると（トレースサイズがGB単位になってくると）実用的でなくなる．CoverageImpact は簡単だが正確性は（著しく）欠ける．これら両方と，Static Slicing を比較するとやはり Static Slicing のほうが大きい結果を返す．このあたりは，いつものトレードオフの問題．

これらの両方を組み合わせられるような手法を考えたい，というところで終わっている．

_ [論文] 機械学習のデバッグ適用 ▲

ICSE 2004 Technical Papers, Dynamic Analysis より．

Yuriy Brun, Michael D. Ernst:Finding latent code errors via machine learning over program executions.Proceedings of ICSE 2004, pp.480-490.

実行するのが高価であったり，テストケースをこれ以上思いつかない，といった場合に，プログラムにまだ見つけていないエラーが残ってないかどうか調べる方法を考えようという論文．

機械学習を使って，エラーのあるコードから抽出された特徴と，エラーの除去されたコードから抽出された特徴とで学習を行い，新たなプログラムから抽出した特徴のうちどれがエラーだと予想されるかを分類する．

特徴として使うのは，動的解析でも静的解析でも使える，と主張しているが，この論文では動的解析によって抽出された Dynamic Invariant を題材にしている．「この部分を（過去に）直されたのならここも怪しいはずだ」という推論は興味深いといえば興味深いのだが，まだどんな特徴を抽出すればエラー検出に役立つとかはよくわかっていないのでそのあたりは将来の課題としている．

うまくいったら面白いなーとは思うのだが，機械学習系って， false positive を出しすぎるとみんな信用してくれなくなって使ってくれない，とか心理的作用があるので実用化は難しいような気がするけれど．

_ [論文] 実行時情報からのアーキテクチャ再構成 ▲

ICSE 2004 Technical Papers, Dynamic Analysis より．

Hong Yan, David Garlan, Bradley Schmerl, Jonathan Aldrich, Rick Kazman:DiscoTect: A System for Discovering Architectures from Running Systems.Proceedings of ICSE 2004, pp.470-479.

プログラムの実行時情報を集めて，アーキテクチャモデルを再構成する．手法としては，アーキテクチャに関係したシステムの特定の振る舞いに反応するステートマシンを用意しておいて，各ステートマシンが，その振る舞いが，コンポーネント間の特定の関係を示しているかどうかを判定する．

たとえば PipedReader を持ったインスタンスと，PipedWriter を持ったインスタンスが出現すると，パイプ接続で対話するコネクションではないか，ということで，それらのインスタンスのPipedReader/Writer との対話イベントを監視するステートマシンを動作させ，それらのインスタンスがデータの読み込み・書き込みなどのイベントを起こしてステートマシンが最終状態まで到達したら，パイプ接続だと判定する．

この手法の利点は，実行時情報のモニタができれば実現できること，また，ステートマシンの用意さえ変えれば，同じアーキテクチャが異なる実装方法で実現されていても対応できる．そのかわり，実行時情報を使う都合上，実行された部分しか調査できないし，ステートマシンが対応できないような ad hoc な実装の場合も発見できない．けれど，実行時情報の使い方としては面白いところ．実行時情報の抽象化とかにも使えるかもしれない．

_ [論文] 形式手法を実践しやすくする開発環境 ▲

ICSE 2004 Technical Papers, Analysis Tools より．

Johannes Henkel, Amer Diwan:A Tool for Writing and Debugging Algebraic Specifications.Proceedings of ICSE 2004, pp.449-458.

形式的仕様記述は便利だという主張のわりには使っているプログラマが少ないので，もっと使えるような環境を整備すべきだ，という論文．

用意するのは，ソースコードから形式仕様を抽出するツールと，実行時に，実オブジェクトのデータを使いながら仕様をチェックするツール．項書き換えで，途中で止まってしまった場合，仕様が不完全だよーとユーザに提示する，らしい．仕様抽出ツールで発見された仕様を徐々に直しながら使っていくことができる．

LinkedList.java の39個のメソッドをカバーするのに100個以上の axioms が要るらしいのですべてのクラスに仕様記述するというのは大変そう．開発者がどれだけ仕様記述に慣れているかにも依存する．

仕様で書ききれない外部メソッド（equals(A, B)など）は，直接 Java コードを呼んで結果を解釈したりもしようとしているので，かなり実用に向けた考え方はしているみたい．

_ 特許 ▲

マイクロソフトがTODOリストの特許取得．特許の内容よりも，TODOリストが「やることリスト」と書かれていたことにちょっとショック．http://www.itmedia.co.jp/news/articles/0406/09/news010.html 特許の原文． 特許の内容をちらっと見た限りでは，Eclipse のTODOリスト＋Java タスクタグがやばそうな感じ．コンパイルエラーの赤線表示＆タスク表示ってVisual J++ の頃からあるものだし．当時はあまり目立たなかったような気がするけど．

_ 日記CGI ▲

ひっそりと日記のアクセス解析はじめました．あきたらやめます．

_ 論文 ▲

ICSE 2004 Technical Papers, Decentralized Systems より．

Nathan D. Ryan, Alexander L. Wolf:Using Event-Based Translation to Support Dynamic Protocol Evolution.

プロトコルからメッセージへと変換するようなトランスレータをプロトコルの状態機械としての仕様から生成してプロトコルでの一連の対話からイベントを生成，イベントからまた対応するプロトコルに変換する，というように「イベント」概念を挿むことでプロトコル間の相互変換を行おう，という研究っぽい．

プロトコルとイベントの相互変換というのは，単なるネットワークプロトコル以外にも適用できるし，異なるプロトコルをしゃべるコンポーネントをイベントでつなぐ以外に，終端がイベントドリブンで真ん中をネットワークでつなぐとか，色々使い道はある．Conceptualの対応が取れないとだめだが．

まだ formalize とかされているわけではなく，何か特別新しいという感じはしない．この先の発展し方次第だろうか．

_ 授業 ▲

JUnit with Eclipse な授業が無事終了．

Eclipse プラグインを探してみて〜という課題を出した結果，SimScan とかいうコード類似部分（コードクローン）検出ツールとか，その他，いくつか微妙なものがレポートとして提出されていた．

上記の結果なども含めて，授業資料などはこちら．http://sel.ist.osaka-u.ac.jp/~t-isio/sd2004/

ベース資料は，http://www.aptest.com/resources.html達人プログラマー（The Pragmatic Programmer），XP本，オブジェクト指向入門（MeyerのEiffel本），など．ちょうどタイムリーな記事なんかもあったりして．http://itpro.nikkeibp.co.jp/free/ITPro/OPINION/20040531/145101/

_ 論文 ▲

ICSE 2004 Technical Papers, Process and Project Management より．

Peter Manhart, Kurt Schneider:Breaking the Ice for Agile Development of Embedded Software:An Industry Experience Report.Proceedings of ICSE 2004, pp.378-386.

組み込み系のソフトウェア開発にアジャイル系のアプローチ（主に単体テスト自動化）を取り込んでみよう，という話．GQM パラダイムをベースに改善してみたらちゃんと効果はあったよーということらしい．

_ 論文 ▲

ICSE 2004 Technical Pepers, Testing II より．

Saurabh Sinha, Alessandro Orso, Mary Jean Harrold:Automated Support for Development, Maintenance, and Testingin the Presence of Implicit Control Flow.Proceedings of ICSE 2004, pp.336-345.

例外による実行パスを考慮した作業サポートツールの実験．手法については interprocedural cfg を使ったとか，簡単に触れられるだけで終わっている．

到達不可能な catch ブロックとか，throw するメソッドから catch までが離れているとか，そういう問題を分析しようというのが目的のように見える．

実験結果を見ると，throw-catch ペアごとのカバレッジなんかは実はけっこう低いのでテストをサポートするのは重要そう．

ただ，例外まわりのパスは非常に数が多くなるので難しいような気はするけど．throw 文で明示的に投げるものだけが対象だからいいといえばいいのか．

_ 論文 ▲

ICSE 2004 Technical Pepers, Testing II より．

Dirk Beyer, Adam J. Chlipala, Rupak Majumdar:Generating Tests from Counterexamples.

Ｃ言語のモデルチェッカ．プログラムの制御フローオートマトンを構築し，プログラムの各文について，その文に到達するために通過する必要がある制御文の条件式を順番に取得していって，それらを満たすようなテストデータを生成する．到達不可能なデッドコードの検出もできる．

テスト自動化ツールなので，無限ループなどに陥っていつまで経っても到達しないようならタイムアウトするとか，工夫はしているよう．

あまり大きなプログラムになってくると扱いきれないみたい．また，この論文執筆時点では再帰呼び出しが扱えないといった弱点もあるみたい．

_ 論文 ▲

ICSE 2004 Technical Papers, Feature-Based Software Engineering より．

Wei Zhao, Lu Zhang, Yin Liu, Jisau Sun, Fuqing Yang:SNIAFL: Towards a Static Non-Interactive Approach to Feature Location.Proceedings of ICSE 2004, pp.293-303.

ソースコードのどの部分がどの機能を実装しているか，というtraceability の回復に IR 手法とBRCG(ブランチ保存コールグラフ）を使うというもの．

最初に，feature ごとの説明ドキュメントをベクタ空間モデルにマップして，各関数から各 feature への類似度を計算する．で，各 feature ごとに，類似度の高い関数を順番に並べて，類似度に一番格差のあるところ（d[i]-d[i+1] が最大となるi）までの関数群だけを取り出して，その feature の specific function とする．

で，ブランチ関係を保存したコールグラフを使って，specific function を呼び出すようなブランチだけを残してコールグラフの枝刈りをして，relevant function を取り出す．

そして，relevant function として得られた関数のうち，単一の feature にのみ関係しているようなものだけを最終的な specific function とする．おまけとして，BRCG から，feature ごとの擬似的な実行トレースを生成する．

単純な IR 手法や，テストケースの実行を分析する dynamic approach と比べて優れた結果となる．また，擬似的な実行のトレースを出力することによって，dynamic approach のような開発者が準備しないような特殊なテストケースも生成できる．（ただし効率はそんなによくない）

specific function の発見については，この手法が85％に対して，dynamic approach のほうが95％と高い結果を出しているが，静的解析だけでも85％は正しい結果が出たというのはすごいといえばすごい．

_ [論文]ソースコード編集作業の分析 ▲

aosd-discuss ML で紹介されていた論文をちらっと読んでみる．

Martin P. Robillard, Gail C. Murphy:Automatically Inferring Concern Code from Program Investigation Activities.Proceedings of 18th International Conference on Automated Software Engineering, pp.225-234, October 2003.

ある concern に関係したコードを変更するとき，複数の場所に分散したコードをあちこち見たりしながら作業を進めていくのが普通なので，そのエディタの操作情報を集めていくことで（どんなソースコードを見ていったか記録することで），その作業時に必要な情報はどのあたりにあるのか，とか開発者の作業を補助しようというもの．

修正作業を，調査イベントの順序付き集合transcript E = { e1, e2, ..., en } として捉えると，イベント e = (D, c, X) はc がアクションの種類（エディタの切り替えとか検索とか）でD がエディタに表示されているメソッド，フィールドでX がアクションごとの追加情報（検索して見つけたメソッドとか）．で，検索対象として見つかったようなエレメントのほうが重みを大きくして，どれかを見ただろうという確率を計算する．

で，全イベントで１度でも閲覧された要素をリストアップして，各要素間の関係の強さを計算する．ある二つの要素について，一方を閲覧したアクションの次のアクションでもう一方を閲覧していたら，何らかの関係があるだろう，と考える．

途中の重み計算のパラメータの影響を強く受けているみたいだが，探している作業という頼りないものがベースのわりにはそれなりの結果が出ている気がする．ただ，いつからが調査でいつからがコーディングだとかいった情報がそれなりに必要？また，false positive も出てしまう（仕方がないが）．

単体で使うよりは，他と組み合わせたほうがうれしいかもしれない．スライシングとか concept analysis とか．個人的には面白いと思うけど．

プログラム変更履歴における「誰々もこの辺りを見ていたよ」という協調フィルタリングにノリとしては近いかもしれない．

_ ニュース ▲

コンピュータの埃からの有害物質の検出とかの話．

具体的数値とか載ってます．http://www.computertakeback.com/the_problem/bfr.cfm

ネタはこちら．http://nikkeibp.jp/wcs/leaf/CID/onair/jp/it/311922

部室とかで多数の PC を一度に掃除するときは少し気をつけたほうがいいかも？

_ 日記CGI ▲

国際会議があるたびに論文ネタで埋め尽くされてしまうので，やっぱりカテゴリごとの最終更新くらいは表示されるようにしようかしら．

実体データは XML なのでカテゴリ情報とかの追加は楽なのだが，そこから最新情報だけ切り出しておくのが面倒だったりする．今のところカテゴリ割り当ても何もやってないし．

_ 論文 ▲

ICSE 2004 Technical Papers, Emirical Methods より．

Parastoo Mohagheghi, Reidar Conradi, Ole M. Kili, Henrik Schwarz:An Empirical Study of Software Reuse vs. Defect-Density and Stability.Proceedings of ICSE 2004, pp.282-291.

ソフトウェアの再利用は品質向上に役立つのか？という仮説に対する実験論文．数値の材料としては defect-density （コード量に対する問題の個数）を使う．

１社（Ericsson）のプロジェクトデータなのでexternal validity としては注意が必要だが，この手の実験データを出してる論文は少ないので比較しようがない気がする．

Accept された仮説:再利用コンポーネントは，non-reused コンポーネントと比べて低い defect-density となる．

Reject された仮設:再利用コンポーネントの defect-density はnon-reused コンポーネントと同じである．

non-reused コンポーネントについて，欠陥の個数と，コンポーネントのサイズは関係しない．

再利用コンポーネントとnon-reused コンポーネントは同じように変更される．

再利用コンポーネントのほうがnon-reused コンポーネントよりも変更される．

棄却できなかった仮説:すべてのコンポーネントについて，欠陥の個数と，コンポーネントのサイズは関連がない．

再利用されたコンポーネントについて，欠陥の個数と，コンポーネントのサイズは関連がない．

defect-density とコンポーネントのサイズは関連がない．（すべてのコンポーネントについての場合でも， また再利用コンポーネントに限った場合でも， non-reused に限った場合でも棄却できない）

_ 論文 ▲

ICSE 2004 Technical Papers, Unified Modeling Language より．

Tewfik Ziadi, Loic Helouet, Jean Marc Jezequel:Revisiting Statechart Synthesis with an Algebraic Approach.Proceedings of ICSE 2004, pp.242-

UML 2.0 シーケンス図からステートチャートを合成しようという試み．各オブジェクトに注目して，メッセージの送受信をイベントとみなして状態遷移が起こると考える．で，シナリオごとに生成したステートチャートを合成して大きなステートチャートを構成する．各シナリオの合成したシナリオ（シーケンス図を含んだシーケンス図）が記述できるようになったことや，ループ記述などができるようになったことが大きいらしい．

でもシーケンス図以外からなら（テキストなどで）合成はできたような気がするのだが……．新規性というか，ネタとしての新しさはあんまり感じられないが，実際にアルゴリズムを明示してがんばっているのはかなり偉いかも．

_ 論文 ▲

ICSE 2004 Technical Papers, Verification より．

Dimitra Giannakopoulou, Corina S. Pasareanu, Jamieson M. Cobleigh:Assume-guarantee Verification of Source Code with Design-Level Assumptions.Proceedings of ICSE 2004, p.211-220.

いわゆるモデルチェック手法．状態の爆発を防ぐために，Assume-guarantee 手法というのを用いている．具体的には，＜Ａ＞ Ｍ ＜Ｐ＞ という３項組で，モジュールＭが動作している環境で，仮定Ａが成立しているときＰが成立するのであれば式全体が true になる．で，二つ部品があるとき＜Ａ＞Ｍ1＜Ｐ＞＜true＞Ｍ2＜Ａ＞が両方とも成立しているのであれば＜true＞Ｍ1 + Ｍ2＜Ｐ＞ が成立する．確認したいプロパティＰが成立するかどうかはＭ1とＭ2についてそれぞれモデルチェックを行えばよいので問題の規模を小さくすることができる．途中の＜Ａ＞をうまく作れたら良い．

設計時は Labelled Transition System としてモデル構築して，実装時は，Ｍ1とＭ2に対応するコンポーネントを構築したら，メソッド単位の呼び出し監視とかを使って本当に条件を満たしているかどうかをテストする．

いちおう（１個だけ）実験もしていて，全体を検査するよりは分割しているほうが明らかにコスト的に優位に立っている．

アイディアとしては，モジュール単位での境界を置くタイプだが仮定Ａの作り方次第では，クラス単位などよりも自由な分割ができそうなので面白いかもしれない．

_ 論文 ▲

ICSE 2004 Technical Papers, Quality of Service より．

Eric Wohlstadter, Stefan Tai, Thomas Mikalsen, Isabelle Rouvelleou, and Premkumar Devanbu:GlueQoS: Middleware to Sweeten Quality-of-Service Policy Interactions.Proceedings of ICSE 2004, pp.189-199.

１つの Web サービスが１つのコンポーネントとみなせるようなサービス指向の環境下で，コンポーネント間でのQoS ポリシーの制御を行う手法．

基本的には，各コンポーネントごとに，サービスに関する述語（cpu_load ＜ 0.5 など）を記述して，ポリシーを呼び出す段階でマッチングを取ってコンポーネント間でのやり取りを行っても大丈夫かどうかをチェックする．

基本的にはコンポーネントと QoS 記述は分離しておくべきだという立場．QoS をサーバで集中管理するのは現実的でないので（今後分散環境での Web サービスが主流となると考えると），各コンポーネントが「自分はこういうポリシーだ」と持っている情報を交換できるようなミドルウェアでの実現となっている．