| 研究課題/領域番号 |
23K16865
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
張 振亜 九州大学, システム情報科学研究院, 助教 (10971228)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2025-03-31
|
| 研究課題ステータス |
完了 (2024年度)
|
| 配分額 *注記 |
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 / Quality assurance / Formal verification / Signal Temporal Logic / Testing / Cyber Physical Systems / Runtime verification |
|---|
| 研究開始時の研究の概要 |
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.
|
| 研究成果の概要 |
Causation monitoringの理論的基盤を確立し、新たなモニタリング方法を物理情報システム（CPS）の品質保証に応用した。CAV'23では、信号時相論理（STL）のcausation monitoringを提案し、従来の手法と比較すると、より多くの情報を報告でき、情報のmasking問題を解決できた。
FM'24では、効率的なモニタリングアルゴリズムを提案した。関連技術をCPSの品質保証に応用し、トレース合成（CAV'24）、ベンチマーク合成（TCAD'25）、AI-CPSの故障解析（TOSEM'24、GECCO'24）、自動運転システムのテスト（ASE'24）にも取り組んだ。
|
| 研究成果の学術的意義や社会的意義 |
本研究は、物理情報システム（CPS）の品質保証に対する新たなアプローチを提供した。本手法は、CPSの実行をランタイムにおいて信号時相論理に基づいて自動的にモニタリングすることができ、従来手法と比較すると、仕様違反の因果関係を報告できるため、システムの故障解析や修復を容易にした。
軽量的な形式手法として、我々のアプローチはCPSの振る舞いを厳密かつ実用的に評価する方法を提供した。現在、CPSはセーフティクリティカルな分野で急速に導入が進んでおり、自動運転システムなどのAIベースのシステムも増加し、このような状況を踏まえると、我々の手法は現実環境におけるCPSの安全保証に対し極めて重要である。
|
