endless pulse

どっくんどっくんふるえる毎日を過ごしています

Java-MOP:A Monitoring Oriented Programming Environment for Java

思い出した頃にこういうことを書く、っていう感じになってきているw
もう少しちゃんと書いて行きますすいません。
ていうか前のブログから少し写そう写そうと思って放置してますね。まあTigerの話なんでそろそろいらないかも知れないけど。(ぇ)


"Java-MOP:A Monitoring Oriented Programming Environment for Java" Feng Chen and Grigore Rossu 2005(たぶん)

概要

1 導入
 この論文では、Java用の監視指向プログラミング(MOP)というソフトウェア開発・解析環境について説明する。それは、Java-MOPと呼ばれている。仕様と実装は共にシステムを形作り、設計によって相互に関係しあうという考えを基に、MOPのフレームワークをソフトウェアの質の向上のために提案する。
 関連研究として、契約プログラミング(DBC)(例:JASS, JML)や、実行時検証(RV)(例:JAVA-MAC, TEMPORAL ROVER, DB ROVER, JPAX, EAGLE, JMPAX)などがある。
 これらの方法とMOPの違いは、新しい論理にも拡張可能であることと、おかしい動きをしたときにセルフ・リカバリできることである。万能な論理というものはない。だけれどもプログラミング言語は万能でなければいけない。だからMOPは目的としているプログラミング言語上にロジックプラグインとして論理を追加できるのである。
 監視は、複雑なソフトウェアシステムの正当性における質・頑健性・信頼性を高める強い土台を提供できる。


2 Java-MOPの概要
 Java-MOPは、MOPの理論的枠組みをサポートしたJava用の開発ツールである。GUIコマンドラインインタフェースと両方を提供している。ユーザが使いやすい形式仕様言語を使用することができる。それが入っていない場合はロジック・プラグインとして新たに組み込める。また、実行時にエラーが出たときに復旧する処理も指定できる。以下にJava-MOPの主要な特徴だけを述べる。興味がわいた読者は私たちのウェブサイト(Mop website)をにパッケージ配布や最新のドキュメントがあるので参照してね。
 拡張可能なアーキテクチャ Java-MOPは図1に示したような分割されたアーキテクチャをとっている。そのため、論理形式のフレームワークを拡張したいときに新しいコンポーネントをシステムに追加できる。それを、ロジック・プラグインと呼んでいる。このコンポーネントは2つのモジュールを含んでいる。ロジック・エンジン言語シェルである。例えば、拡張正規言語(ERE)用のロジックエンジンとERE用のJavaのシェルが、ERE用のロジックプラグインを構成している。ロジックエンジンは、ある抽象的な表現(疑似コード)で表される効果的なモニタに論理式を変換する(translate)。そして言語シェルが抽象的なモニタを特定の言語(例えば、Java)のコードに変換する(transform)。単純な仕様言語や、プログラミング言語仕様形式(Jassなど)のときは、ロジックエンジンが必要なく、言語シェルだけでモニタを作るのに十分なときもある。
 クライアント側の部分では、Javaの注釈プロセッサを含む。それは、モニタの構成の特徴に従って生み出されたモニタリングコードを統合する。加えて、クライアント側の部分では監視されるイベントを生み出すためのコードを実装する役割も担う。現在では、Java-MOPはAspectJを実装の機構として使用している。しかしAspectJは実行時の限界も示唆している。AspectJを用いて統合されたものは静的であるが、監視というのは動的である。これは、動的な要素の監視のときにトラブルのもとになり、非効率的である。例えば、不変のクラスがあったとき、そのクラスがanObjectと同じすべてのオブジェクトのafieldの代わりにanObject.aFieldの更新を毎回監視する必要があるかもしれない。
 モニタ統合 すべてのロジック・プラグインは、仕様形式のためのモニタリングコードを統合するため、本質的にアルゴリズムエンコードする。(←よくわからない;;)EREやJASS、JMLと同じように未来時間時相論理や過去時間時相論理のモニタ統合アルゴリズムを考案した。
 - JML、JASS : DBCに基づいたアプローチは、仕様にコードをを含め、実行時に検査するためにプレコンパイルするという考えを導く。そのため、Java-MOPにそれらを含めるのはスムーズにできる。JMLやJASS注釈のオリジナルのシンタックスとは少しだけ変更してある。
 - 時相論理 : 時相論理は、システムの形式仕様と検証の分野で、必要不可欠な表現が豊かな形式である。時相論理とは異なる、過去と未来の時間を扱えるロジックプラグインを提供する。
 - ERE : 正規表現は要求を監視することにおいて的確で強力な仕様言語を提供する。なぜなら、プログラムの実行とレースは実際状態の文字列だからだ。EREは正規表現に相補性を加えたものである。Java-MopにERE用のロジックプラグインが組み込んである。
 モニタの振る舞いの操作 テストにより厳密さを加えることに加えて、MOPは、プログラム実行中の正しさを保証するためのモニタリングツールである。実行時リカバリをサポートするために、MOPは、要求が破られるか満たされたときに、プログラムの実行を操作することができる。例えば、状態をリセットして、システムをリブートする、という操作を設定できる。
 MOPモニタは異なった実行時のスコープを持てる。不変クラスでは、クラスの状態の変化を毎回チェックできる。また、インタフェースの制限がかかっていれば、クライアントがクラスからインタフェースを作ったときにチェックする。Java-Mopではメソッドの前後の状態やチェックポイントアサーションもサポートしている。加えて、結果を同期するか非同期なのかも選択できる。非同期の方が実行時のオーバーヘッドは少ない。


3 結論
 この論文では、MOPの理念をサポートしている、Java用の開発・解析環境を紹介した。モニタは形式仕様から生み出され、システムの実行時に検証するために使われる。ユーザは仕様に違反したときの、セルフリカバリの動作を定義できる。異なった領域の要求に対応するために、有用な仕様記述言語のロジックプラグインもよりたくさんJava-MOPに加えられるだろう。


感想

とりあえず上のが概要じゃないw直訳だ。
参考文献を入れないと3ページ半の文章だったのでこんな私でも一日で読めました。一度MOPの内容は拾っているし楽だった。浅い話しかしてないしねw
未来時間時相論理(future time temporal logic)とか過去時間時相論理(past time temporal logic)は、前読んだ論文でも見たけど面白かった。ただやっぱりこれで書き下すのは大変だよね…。どうしたらいいのかしら。拡張正規表現(ERE)ってどうなんだろう。あんまり調べてないけど。契約プログラミング(DBC)についても全然知らない。ああー勉強することが多い。AspectJについても知らなきゃな。

一旦Java-MOPは使ってみよう。GUIベースのものはEclipseプラグインとして配布されている模様なので明日試してみる。その上で、発表する内容を吟味しよう。。Java-MOPのプロトタイプの評価の論文や、Java-MOPを拡張しましたという論文があったりするので。両方から参照できると面白いのかもしれないけど、時間的な問題もあるし。
今MOPについて思っているのは、

  • 仕様書きにくいだろうな→書きやすくするための機構?
  • Java以外への発展は?必要なのはC言語とかコアな言語?それとも関数型?個人的にはRubyでやりたいけど理由が見つからないwAspectRとかあるんだけどどうなの?

あたりかな。せっかく「テスト」と「形式検証」の間をとって、手軽にバグ無しチェック!とか言っているのだから、実行するためのコストを減らしたい。今のままじゃ大して形式仕様とコスト変わらないんじゃ?と思えてしまう。まだ論文2つめだけど。要約できる癖つけたい。