| 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 |
張 振亜 九州大学, システム情報科学研究院, 助教 (10971228)
|
|---|
| Project Period (FY) |
2023-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| 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 / Testing / Cyber Physical Systems / Runtime verification / Quality assurance |
|---|
| 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 Annual Research Achievements |
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.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
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.
|
| Strategy for Future Research Activity |
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.
|
