| Project/Area Number |
23K16865
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
Zhang Zhenya 九州大学, システム情報科学研究院, 助教 (10971228)
|
|---|
| Project Period (FY) |
2023-04-01 – 2025-03-31
|
| Project Status |
Completed (Fiscal Year 2024)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2023: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
|
|---|
| Keywords | Monitoring / Signal temporal logic / Cyber-physical systems / Formal methods / Quality assurance / Formal verification / Signal Temporal Logic / Testing / Cyber Physical Systems / Runtime verification |
|---|
| Outline of Research at the Start |
Cyber-Physical Systems are safety-critical and their quality assurance is important. First, we refine the semantics of Signal Temporal Logic such that it delivers more information about system evolution. Moreover, we apply the refined semantics to develop more effective quality assurance techniques.
|
| Outline of Final Research Achievements |
By the outcome of this research, we establish the theoretical foundation of causation monitoring, and apply this new monitoring paradigm in quality assurance of cyber-physical systems (CPS). First, in CAV'23, we propose the causation semantics of signal temporal logic (STL), which can also be seen as a novel online monitoring approach. Compared to existing approach, causation monitoring can report more information regarding system evolution, solving the information masking problem in existing monitoring approach.
Based on this result, in FM'24 we propose an efficient monitoring algorithm that makes causation monitoring applicable to real systems. We apply related techniques to CPS quality assurance, including trace synthesis (CAV'24), benchmark synthesis (TCAD'25), fault analysis of AI-enabled CPS (TOSEM'24, GECCO'24), etc. Moreover, we also explore testing of autonomous driving systems in ASE'24, which wins the ACM SIGSOFT Distinguished Paper Award.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究は、物理情報システム（CPS）の品質保証に対する新たなアプローチを提供した。本手法は、CPSの実行をランタイムにおいて信号時相論理に基づいて自動的にモニタリングすることができ、従来手法と比較すると、仕様違反の因果関係を報告できるため、システムの故障解析や修復を容易にした。
軽量的な形式手法として、我々のアプローチはCPSの振る舞いを厳密かつ実用的に評価する方法を提供した。現在、CPSはセーフティクリティカルな分野で急速に導入が進んでおり、自動運転システムなどのAIベースのシステムも増加し、このような状況を踏まえると、我々の手法は現実環境におけるCPSの安全保証に対し極めて重要である。
|
