Integrated Runtime Monitoring of Network Software by Fusion of Runtime Verification and Model Checking

2016 Fiscal Year Final Research Report

• Project/Area Number: 26280019
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Partial Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Chiba University
• Principal Investigator: Yamamoto Mitsuharu 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
• Co-Investigator(Kenkyū-buntansha): 萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252) ; Artho Cyrille 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (30462831) ; 山形 頼之 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415758) ; 田辺 良則 鶴見大学, 文学部, 教授 (60443199)
• Research Collaborator: KOHAN Alexander 千葉大学 ; WEITL Franz 千葉大学 ; MA Lei 千葉大学 ; SEBIH Nazim 東京大学
• Project Period (FY): 2014-04-01 – 2017-03-31
• Keywords: 実環境モデル検査 / 実行時検証 / ネットワークソフトウェア

Outline of Final Research Achievements

By fusing runtime verification and model checking, we proposed a framework to verify global specification of network systems with taking account of thread scheduling nondeterminism of the system under test, and implemented its prototype.
Runtime verification alone cannot deal with thread scheduling nondeterminism, and model checking alone cannot handle properties of the whole network system consisting of the system under test and remote peers. By fusing both techniques, we made it possible to detect bugs that cannot be manifested only by existing model checking against the system under test.

Free Research Field

情報数理学