| Project/Area Number |
24K23861
|
|---|
| Research Category |
Grant-in-Aid for Research Activity Start-up
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
1001:Information science, computer engineering, and related fields
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
Hsieh Chiao (謝橋) 京都大学, 情報学研究科, 特定助教 (71006426)
|
|---|
| Project Period (FY) |
2024-07-31 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2025: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2024: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 形式検証 / サイバーフィジカルシステム / 安定性解析 / ブラックボックスモデル |
|---|
| Outline of Research at the Start |
Verification and validation (V&V) is a crucial procedure for certifying the safety of cyber-physical systems (CPS) such as self-driving cars. The goal is to certify the safety through rigorous analyses on mathematical models of CPS. This project particularly studies stability analyses on CPS models by only sampling inputs and outputs from CPS, i.e., a black box approach. The project further aims to address high volume of samples and speed up the stability analysis by parallelization. PI believes that this is a step toward a practical V&V framework for safety-critical CPS in the future.
|
| Outline of Annual Research Achievements |
This year, PI followed the project proposal to achieve the expected result in Phase 1. The major goal in Phase 1 is to establish a baseline black-box analysis for certifying the Lyapunov stability of continuous-time dynamics. Combining the recent idea of sampling and exploiting Lipschitz continuity to approximate the continuous-time dynamics, PI developed a new analysis based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis, and PI extended the analysis with parallelized verification for different regions of the state space. This new analysis has significant reduced the number of required samples for certifying the stability of 2D and 3D systems compared with the existing analysis. In addition, PI provided a rigorous termination guarantee to ensure the analysis will always finish and answer if the continuous-time dynamics is provably stable, or no proofs can be found in the predefined hypothesis space.
PI has coauthored and submitted a research conference paper summarizing the research outcome in this study, and the paper is accepted by and will be published in the 28th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2025) in May 2025.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
PI has developed a new black-box analysis as planned, and the analysis has shown great improvement over the existing analysis. The research paper is further accepted by the top international conference.
|
| Strategy for Future Research Activity |
Next year, PI plans to follow the project proposal and achieve the goal for Phase 2. The major goal in Phase 2 is to extend the above-mentioned baseline analysis to support hybrid systems with both continuous-time dynamics and discrete-time transitions. This will enable the analysis on more realistic cyber-physical systems. PI also plans to improve the baseline analysis to handle systems with 4D or more dimensions by better parallelization and optimization techniques.
|
