Constraint Acquisition and Compositional Verification of Large and Complex Cyber-Physical Systems
| Project/Area Number |
22K11969
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2025: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2024: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2023: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | サイバーフィジカルシステム / 制約獲得 / 部品化検証 / 運転支援システム / 制約プログラミング |
|---|
| Outline of Research at the Start |
本研究では大規模複雑なサイバーフィジカルシステム（CPS）の検証に取り組む．ロボットや車などのCPSが普及しつつあるが，安全性が十分に検証されていない問題がある．実装の大規模化と，機械学習の導入による複雑化が進み，形式的な検証が難しくなっている．その解決策として，対象CPSを部品に分割して検証するアプローチがあるが，部品から構成するモデル化や，各部品の入出力に関する制約（契約）の獲得が課題となる．そこで，機械学習部品とそうでない部品ごとに検証する手法，制約獲得する手法，それらの結果からCPS全体を検証する手法の研究に取り組む．
|
| Outline of Annual Research Achievements |
大規模複雑なサイバーフィジカルシステム（CPS）の制約獲得や部品化検証を可能にすることを目標に，2つの研究項目を実施した．
（1）サイバーフィジカルシステムをモデル化した同期リアクティブシステムの部品化検証手法を提案した．本研究では階層的なシステム，とくに部品ごとに契約を付与して記述されたシステムを対象とした．対象システムを部品の並列合成とみなし，assume-guarantee検証を実施するための手法を提案した．提案手法では，システム記述を有向ハイパーグラフとみなし，部分グラフの分離として部品化を定式化する．この分離処理は制約獲得処理とみなすことができ，獲得した制約についてSMTソルバー等を用いて検証を実施すれば，プロセスの自動化が可能である．提案手法をSMTモデル検査器の上に実装し，循環構造をもつシステムの自動検証を可能にした．提案手法について論文を執筆・投稿し，国際会議SPINに採択された．
（2）運転者の眠気検知（DDD）手法について研究した．車両情報を用いた深層学習による高性能なDDDを実現することを目的に，ヨー角速度の予測と実測値の比較による異常判定からDDDを行う手法を提案した．予測には深層学習モデルと逐次最小2乗法（RLS法）を用いて同定した差分方程式モデルを用いた．また正解データとして被験者の脳波を用いた．運転シミュレータCARLA上で被験者が運転を実施する実験から，車両情報データと脳波データを収集し，その後，実装したモデルについて評価する実験をおこなった．それぞれのモデルに対し異常検知の性能をROC曲線に基づき評価し，深層学習モデルがRLS法によるモデルよりも高性能であることを示す結果を得た．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実施計画に従い研究を進め，一定の成果を得ることができた．
研究項目（1）では，大規模複雑CPSを自動検証するための手法を開発した．SMTソルバーを用いた既存の部品化検証ツールが課題としていた，部品ごとの契約が互いに参照し合う循環系の扱いを改善することができた．CPSモデルがフィードバックループを含む場合等に有用だと考えられる．一方，実際的な例への応用は今後の課題である．
研究項目（2）では，深層学習によるDDDシステムを構築し，その有効性を実験で確かめることができた．DDD手法とシステムは多数提案されているため，それらとの比較が今後の課題である．
|
| Strategy for Future Research Activity |
制約獲得と部品化検証の手法を明らかにし，大規模複雑CPSの検証を可能にするため，以下の研究項目に取り組む．
【A．部品化検証や制約獲得手法の形式化】CPSモデルの部品記述や部品化検証手法が複数提案されている．検証プロセスを簡単化したり，自動検証を促進するための研究に取り組む．たとえば，同一の形式化の枠組み内で既存の部品記述手法の表現力を比較したり，新たな部品化と自動検証の手法を検討したり，ML系をモデル化した部品を扱う方法を検討したりする．
【B．自動運転プラットフォームへの応用】同期リアクティブシステムの実際的な例として，自動運転プラットフォームのプランニングや制御に関する部品をモデル化し，安全性を検証する実験をおこなう．必要に応じて部品化や制約獲得の手法を検討する．
【C．DDD手法の品質に関する議論】DDD手法についてサーベイを実施し，既存手法との詳細な比較をおこなう．DDDの性能や信頼性について，既存手法における評価方法の差異や，不足している論点に関する議論を，統合的・形式的に記述する．あわせて，提案手法を用いた実験を実施し，議論を補強する．既存のDDDシステムに較べて高性能かつ高信頼なシステムの実現を目指す．また，そのようなシステム開発のプロセスを明らかにすることを目指す．
|
Report
(2 results)
Research Products
(6 results)
