研究課題
本研究課題の最終年度である本年度は、これまでの研究成果を論文としてまとめ、発表するとともに、本課題における成果を総括し、続く課題あるいは関連する研究課題におけるさらなる発展の可能性や方向性について検討を行った。前年度のうちに、我々の先行研究課題および本課題の前年度までの成果をまとめた雑誌論文を提出していたが、今年度は現在査読者からのコメントに従って修正・加筆を行い、掲載が決定した。我々がモデル検査器の基盤として用いているJava PathFinderがネットワークAPIとして使用するモデルクラスとして、先行研究課題ではJava.ioクラスの実装を与えていたが、本課題ではより多くのネットワークアプリケーションに対する検証を可能とするために、ノンブロッキングI/Oを含むJava.nioクラスの実装を継続して行っていた。今年度はこの成果を論文としてまとめて投稿し、ソフトウェア工学分野のトップカンファレンスの一つであるASEに採択された。モデルクラスがノンブロッキング処理や例外処理を正しく処理できているか確認するために、モデルベースのテストツールModbatを開発してそれを用いたこと、検証の実例として、Javaで実装されているHTTPサーバRupyの実際のバグを発見したことが特徴となっている。研究期間の締め括りである2014年3月にはSGT Inc.からNastaran Shafiei氏を招き、研究グループ内外のメンバーとともにラップアップセミナーを開催した。同氏はJava PathFinderにおいてnative methodのモデリングを自動的・半自動的に行うjpf-nhandlerのメイン開発者である。セミナーおよび続くテクニカルミーティングにおいては、我々が対象とするネットワークAPIについてjpf-nhandlerとの連携について議論した。この結果は我々の研究グループにおける後続研究課題において発展的に生かされるものと考えている。研究協力者 ヴァイテル・フランツ (千葉大学) セビ・ナジム (東京大学)
25年度が最終年度であるため、記入しない。
すべて 2014 2013 その他
すべて 雑誌論文 (3件) (うち査読あり 3件) 備考 (1件)
IEEE Transactions on Software Engineering
巻: Vol.40, No. 5 ページ: 483-501
10.1109/TSE.2013.49
Hardware and Software: Verification and Testing, 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings
巻: LNCS 8244 ページ: 112-128
10.1007/978-3-319-03077-7_8
28th IEEE/ACM International Conference on Automated Software Engineering (ASE)
巻: なし ページ: 169-179
10.1109/ASE.2013.6693077
http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache
