2016 Fiscal Year Annual Research Report
Integrated Runtime Monitoring of Network Software by Fusion of Runtime Verification and Model Checking
| Project/Area Number |
26280019
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
Artho Cyrille 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (30462831) [Withdrawn]
山形 頼之 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415758)
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 実環境モデル検査 / 実行時検証 / ネットワークソフトウェア |
|---|
| Outline of Annual Research Achievements |
研究期間全体を通して、以下の3つの部品それぞれに対応するサブプロジェクトに分割して研究を進めている。(1) net-iocache: ネットワーク環境において検査対象を管理するためのJava Pathfinder(JPF)拡張。(2) net-monitor: JPF内外のネットワークプロセスからイベントを収集し、実行監視による実行時検査を行う部分。最終的にはnet-iocacheと統合される。(3) peer-monitor: 通信相手のプロセスからnet-monitorにイベントを送るツール。
(1)については、net-iocacheの実装としては前年度まででほぼ完成している。JPFを用いた検証をより広い範囲で行えるようにするため、JPFをAndroidの実機上で動作させるjpf-mobileを実装し、論文として発表した。(2)については、実行監視部分とモデル検査器を統合するnet-monitoringフレームワークの基本設計および、チャットサーバを用いた実証実験の結果をショートペーパーとしてまとめ、発表した。(3)については、前年度に実行監視のための論理/形式体系として設計したフレームワークCSP_EおよびそれのScala上の検査器について、実例を用いた既存体系との比較、形式的意味論の構築を行い、論文として発表した。CSP_Eはプロセス代数CSPに基づく実行監視のためのフレームワークであり、並行システムをボトムアップに記述できる。これは既存のオートマトンベースの監視フレームワークQEAがトップダウンに記述するのと対照的であり、システムコンポーネント間の正しいやりとりを記述しやすくすることを目的としている。
研究協力者 馬雷 (千葉大学) ヴァイテル・フランツ (千葉大学) コハン・アレクサンダー (千葉大学)
|
| Research Progress Status |
28年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
28年度が最終年度であるため、記入しない。
|
| Causes of Carryover |
28年度が最終年度であるため、記入しない。
|
| Expenditure Plan for Carryover Budget |
28年度が最終年度であるため、記入しない。
|
Research Products
(4 results)
-
[Journal Article] Model-based API Testing of Apache ZooKeeper2017
Author(s)
Cyrille Valentin Artho, Quentin Gros, Guillaume Rousset, Kazuaki Banzai, Lei Ma, Takashi Kitamura, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto
-
Journal Title
10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
Volume: 印刷中
Pages: 印刷中
Peer Reviewed / Open Access / Acknowledgement Compliant
-
[Journal Article] Java Pathfinder on Android Devices2016
Author(s)
Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho, Yoriyuki Yamagata, Lei Ma, Masami Hagiya, and Yoshinori Tanabe
-
Journal Title
ACM SIGSOFT Software Engineering Notes
Volume: 41(6)
Pages: 1～5
DOI
Peer Reviewed / Open Access / Acknowledgement Compliant
-
[Journal Article] Runtime Monitoring for Concurrent Systems2016
Author(s)
Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, and Mitsuharu Yamamoto
-
Journal Title
Runtime Verification - 16th International Conference, (RV 2016)
Volume: LNCS 10012
Pages: 386～403
DOI
Peer Reviewed / Open Access / Acknowledgement Compliant
-
