| 研究課題/領域番号 |
24K23861
|
|---|
| 研究種目 |
研究活動スタート支援
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
1001:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
Hsieh Chiao (謝橋) 京都大学, 情報学研究科, 特定助教 (71006426)
|
|---|
| 研究期間 (年度) |
2024-07-31 – 2026-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2025年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2024年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
|
|---|
| キーワード | 形式検証 / サイバーフィジカルシステム / 安定性解析 / ブラックボックスモデル |
|---|
| 研究開始時の研究の概要 |
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.
|
| 研究実績の概要 |
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.
|
| 現在までの達成度 |
現在までの達成度
2: おおむね順調に進展している
理由
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.
|
| 今後の研究の推進方策 |
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.
|
