High Reliability Software System Verification(JAXA's Engineering Digital Innovation Center (JEDI), Japan Aerospace Exploration Agency)

Research Staff

  • Professor Naoki ISHIHAMA

    Professor
    Naoki ISHIHAMA

E-mail ishihama@is.naist.jp
To the site https://stage.tksc.jaxa.jp/jedi/JAXAlab/index-e.html
To the JEDI's site https://stage.tksc.jaxa.jp/jedi/en/index.html
Fig.1 The concept of robustness verification and automated environments

Fig.1 The concept of robustness verification and automated environments

Fig.2 An example of assurance methods for verification completeness using assurance cases

Fig.2 An example of assurance methods for verification completeness using assurance cases

Fig.3 JAXA Tsukuba Space Center

Fig.3 JAXA Tsukuba Space Center

Research Areas

Recent embedded systems and infrastructure systems are recognized as the basis for accomplishing national and human safety. Assurance of high reliability in those systems is one of the most critical issues to increase the safety of the whole social system.
Based on the proven studies and practices concerning high reliability and safety in the field of space systems established by JEDI in JAXA, our "High Reliability Software System Verification Laboratory" is focused on research into software verification methodologies to achieve high reliability and safety in software that must function properly under extreme environmental conditions.
Assurance methods for verification completeness, such as End-to-End point of view for complex distributed software systems, are a recent key issue. In our lab, the main topics are reliability and safety verification methodology and reliability and safety assurance methodology.
The research outcomes are expected to be applied to practical uses for systems that require high reliability, not only in space systems but also in social core infrastructures.

Reliability and safety verification methodology

  • Verification methods for robustness
    We research and develop the assurance methods for verification completeness, and the key technologies for robustness verification including the non-functional specifications.
  • Automated verification methods
    We first research the analysis of system configurations, operational conditions and system error pattern models. Based on those concepts, algorithms and methodologies for the automated generation of verification cases and the automated success criteria of verification results are developed.

Reliability and safety assurance methodology

  • Assurance methods for verification completeness
    We research technology to evaluate verification completeness of whole End-to-End software systems based on verification information produced by various software systems.
  • Assurance methods for defect propagation
    We formulate systematic defect modes in the whole software system, then research and demonstrate the evaluation method of propagation effects into whole systems.

Key Features

In the first half of the graduate program, students complete required coursework on NAIST’s campus, and in the last half, determine their of the thesis themes and join the research of various technologies to produce high reliability and safety in systems, such as independent Verification and Validation (IV&V), a model-based verification and system assurance, through project based studies and internships in JAXA. Most of the knowledge and skills experienced in our laboratory are highly concerned with science and industry, not only in the space domain but also in a broad range of industries, such as the automotive industry. Internships in JAXA Tsukuba Space Center are held during this period. For necessary topics, international collaborative studies with other international space agencies such as NASA are also performed.