Software model checking methods for cloud computing middleware

2015 Fiscal Year Final Research Report

• Project/Area Number: 23240003
• Research Category: Grant-in-Aid for Scientific Research (A)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: The University of Tokyo
• Principal Investigator: Hagiya Masami 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
• Co-Investigator(Kenkyū-buntansha): ARTHO Cyrille 産業技術総合研究所, 情報セキュリティセンター, 研究員 (30462831) ; YAMAMOTO Mitsuharu 千葉大学, 大学院理学研究科, 准教授 (00291295) ; TANABE Yoshinori 鶴見大学, 文学部, 教授 (60443199) ; YOKOYAMA Shigetoshi 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (10600968)
• Research Collaborator: WEITL Franz ; POTTER Richard ; LEUNGWATTANAKIT Watcharin
• Project Period (FY): 2011-04-01 – 2016-03-31
• Keywords: 仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング

Outline of Final Research Achievements

We have developed methods of software verification for network applications that are typical in cloud computing environments. Our software model checking tool has been enhanced so that it can handle various protocols and application configuration. We also have developed a novel tool based on model base testing so that we can verify a wider range of applications. The usefulness of the tools has been confirmed by experiments with network applications such as Zookeeper, software for coordination of distributed processes in cloud computing environments.

Free Research Field

ソフトウェア