High Reliability Software System Verification(JAXA's Engineering Digital Innovation Center (JEDI), Japan Aerospace Exploration Agency)
Research Staff
-
Professor
Naoki ISHIHAMA
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.2 An example of assurance methods for verification completeness using assurance cases
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.