2013 Fiscal Year Annual Research Report
分散チェックポインティングを用いたネットワークアプリケーションのモデル検査
| Project/Area Number |
23300004
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
ARTHO Cyrille 独立行政法人産業技術総合研究所, その他部局等, 研究員 (30462831)
田辺 良則 国立情報学研究所, 大学共同利用機関等の部局等, 教授 (60443199)
|
|---|
| Project Period (FY) |
2011-04-01 – 2014-03-31
|
| Keywords | モデル検査 / チェックポインティング |
|---|
| Research Abstract |
本研究課題の最終年度である本年度は、これまでの研究成果を論文としてまとめ、発表するとともに、本課題における成果を総括し、続く課題あるいは関連する研究課題におけるさらなる発展の可能性や方向性について検討を行った。
前年度のうちに、我々の先行研究課題および本課題の前年度までの成果をまとめた雑誌論文を提出していたが、今年度は現在査読者からのコメントに従って修正・加筆を行い、掲載が決定した。
我々がモデル検査器の基盤として用いている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との連携について議論した。この結果は我々の研究グループにおける後続研究課題において発展的に生かされるものと考えている。
研究協力者 ヴァイテル・フランツ (千葉大学) セビ・ナジム (東京大学)
|
| Current Status of Research Progress |
Reason
25年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
25年度が最終年度であるため、記入しない。
|
-
-
[Journal Article] Modbat: A Model-based API Tester for Event-driven Systems2013
Author(s)
C. Artho, A. Biere, M. Hagiya, E. Platon, M. Seidl, Y. Tanabe and M. Yamamoto
-
Journal Title
Hardware and Software: Verification and Testing, 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings
Volume: LNCS 8244
Pages: 112-128
DOI
Peer Reviewed
-
-
