• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Model Checking Network Applications using Distributed Checkpointing

Research Project

Project/Area Number 23300004
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field Software
Research InstitutionChiba University

Principal Investigator

YAMAMOTO Mitsuharu  千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)

Co-Investigator(Kenkyū-buntansha) HAGIYA Masami  東京大学, 情報理工学系研究科, 教授 (30156252)
ARTHO Cyrille  独立行政法人産業技術総合研究所, セキュアシステム研究部門, 主任研究員 (30462831)
TANABE Yoshinori  国立情報学研究所, アーキテクチャ科学系, 特任教授 (60443199)
Research Collaborator LEUNGWATTANAKIT Watcharin  東京大学
WEITL Franz  千葉大学
POTTER Richard  東京大学
SEBIH Nazim  東京大学
Project Period (FY) 2011-04-01 – 2014-03-31
Project Status Completed (Fiscal Year 2013)
Budget Amount *help
¥19,240,000 (Direct Cost: ¥14,800,000、Indirect Cost: ¥4,440,000)
Fiscal Year 2013: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2012: ¥10,140,000 (Direct Cost: ¥7,800,000、Indirect Cost: ¥2,340,000)
Fiscal Year 2011: ¥5,720,000 (Direct Cost: ¥4,400,000、Indirect Cost: ¥1,320,000)
Keywordsモデル検査 / チェックポインティング
Research Abstract

With distributed checkpointing, we enhanced our previous results on model checking network applications so that it can check network applications on more complicated and practical environments. This was accomplished by implementing communication resumption on distributed checkpointing. We also adopted newer network API that is used in practical network applications so as to check wider range of applications.

Report

(4 results)
  • 2013 Annual Research Report   Final Research Report ( PDF )
  • 2012 Annual Research Report
  • 2011 Annual Research Report
  • Research Products

    (9 results)

All 2014 2013 2012 2011 Other

All Journal Article (4 results) (of which Peer Reviewed: 4 results) Presentation (2 results) Remarks (3 results)

  • [Journal Article] Modular Software Model Checking for Distributed Systems2014

    • Author(s)
      Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi
    • Journal Title

      IEEE Transactions on Software Engineering

      Volume: - Issue: 5 Pages: 483-501

    • DOI

      10.1109/tse.2013.49

    • Related Report
      2013 Annual Research Report 2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] Modbat: A Model-Based API Tester for Event-Driven Systems2013

    • Author(s)
      Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, and Mitsuharu Yamamoto
    • Journal Title

      Proceedings of the 9th Haifa Verification Conference, Lecture Notes in Computer Science

      Volume: 8244 Pages: 112-128

    • DOI

      10.1007/978-3-319-03077-7_8

    • ISBN
      9783319030760, 9783319030777
    • Related Report
      2013 Annual Research Report 2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] Software Model Checking for Distributed Systems with Selector-Based, Non-blocking Communication2013

    • Author(s)
      Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto
    • Journal Title

      28th IEEE/ACM International Conference on Automated Software Engineering

      Volume: - Pages: 169-179

    • DOI

      10.1109/ase.2013.6693077

    • Related Report
      2013 Annual Research Report 2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] Model checking distributed systems by combining caching and process checkpointing2011

    • Author(s)
      Watcharin Leungwattanakit
    • Journal Title

      26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)

      Volume: 1 Pages: 103-112

    • DOI

      10.1109/ase.2011.6100043

    • Related Report
      2013 Final Research Report 2011 Annual Research Report
    • Peer Reviewed
  • [Presentation] Modbat : A model-based API tester for event-driven systems2012

    • Author(s)
      Cyrille Artho
    • Organizer
      第10回ディペンダブルシステムワークショップ(DSW2012)
    • Place of Presentation
      独立行政法人理化学研究所計算科学研究機構
    • Related Report
      2013 Final Research Report
  • [Presentation] Modbat: A model-based API tester for event-driven systems2012

    • Author(s)
      Cyrille Artho
    • Organizer
      第10回 ディペンダブルシステムワークショップ (DSW 2012)
    • Place of Presentation
      独立行政法人理化学研究所 計算科学研究機構
    • Related Report
      2012 Annual Research Report
  • [Remarks]

    • URL

      http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache

    • Related Report
      2013 Final Research Report
  • [Remarks] projects/net-iocache - Java Path Finder

    • URL

      http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache

    • Related Report
      2013 Annual Research Report
  • [Remarks]

    • URL

      http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache

    • Related Report
      2011 Annual Research Report

URL: 

Published: 2011-04-06   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi