| 研究課題/領域番号 |
23K16865
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
張 振亜 九州大学, システム情報科学研究院, 助教 (10971228)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2023年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
|
|---|
| キーワード | Monitoring / Signal Temporal Logic / Cyber-physical systems / Formal methods / Testing / Cyber Physical Systems / Runtime verification / Quality assurance |
|---|
| 研究開始時の研究の概要 |
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.
|
| 研究実績の概要 |
The project is going smoothly with a number of scientific research outcomes. There are 8 research papers published or accepted, and there are also a number of papers under submission to international conferences or journals.
First, we published a work in CAV’23 (CORE A*, top-most conference), in which we propose causation monitoring, that can report more information about system evolution than existing monitors. This work builds the theoretical foundation of this project, namely, fine-grained monitoring of Signal Temporal Logic that aims to deliver more information. Based on this work, we do several related applications of signal monitoring, including testing of autonomous driving systems (ISSRE’23, CORE A), object tracking (PR’23, CORE A*), repair of DNN controllers (GECCO’24, CORE A), model checking with complex STL specifications (CAV’24 CORE A*), testing of unmanned aerial vehicles (SBFT’24) etc.
Our ongoing works involve several applications of our fine-grained monitoring technique in different directions. One line is the fault localization and repair of AI-enabled CPS, which requires our causation monitor to provide useful information. Another line is the use of our new semantics in optimal control synthesis, and specifically, we are exploring its application in reinforcement learning for CPS.
We continue our contribution to the ARCH friendly competition, and we co-author the report of falsification tool competition published in ARCH’24.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
The project is going smoothly with a number of scientific research outcomes. We have papers accepted or published in top international conferences or journals, including conferences such as CAV (CORE A*), ISSRE (CORE A), GECCO (CORE A).
By these research outcomes, we have established the theoretical foundation of our project, and now we are moving to the applications of our novel monitoring techniques and STL semantics. Moreover, recently we also come up with an implementation of our causation monitor that is much more efficient than the direct implementation from definition, which allows the application of our causation semantics.
Some of our ongoing works have got preliminary or complete results and are under submission. For instance, our fault localization work extends the classic spectrum-based fault localization in traditional software analysis by leveraging the information provided by our monitoring techniques. We believe these research outcomes will be recognized by the research community.
We also actively participated competitions in community. Notably, we participated in the SBFT'24 tool competition, UAV testing track. Our tool named TUMB wins the 2nd rank among 8 participants, which signifies the effectiveness of our approach.
|
| 今後の研究の推進方策 |
Our ongoing works involve several applications of our fine-grained monitoring technique in different directions.
One line is the fault localization and repair of AI-enabled CPS, which requires our causation monitor to provide useful information. In this research, we extend the spectrum-based fault localization framework to CPS, and our monitoring technique helps in diagnosing faulty intervals during system execution. With this information, we can reduce the potentially suspicious space of fault localization significantly, thereby improving the precision of fault localization.
With results from fault localization, we can perform repair to CPS components. Our preliminary research has been accepted by GECCO'24 (CORE A). We plan to extend this research to explore more effective repair approaches.
Another line is the use of our new semantics in optimal control synthesis, and specifically, we are exploring its application in reinforcement learning for CPS. Preliminary experiments have shown the superiority of our causation semantics over the classic robust semantics of STL in characterizing the states of execution traces. By this, we can devise better reward functions to assist reinforcement learning for optimal control policies.
|
