研究課題
連続・離散ハイブリッドシステムのための制約プログラミング技術を開発することを目標に，MATLAB/Simulinkで記述したモデルを検証・テストする手法について研究した．今年度はおもに3項目を実施した．（1）Simulinkモデルとその安全性について検査する手法について研究した．提案手法は，モデルと安全性を述語論理式に変換し，それを既存のSMTソルバーで解くことにより検査を実施する．今年度は，産業界由来の例を扱うことを目指し，多様なモデルを効率よく検査するための複数の方法を設計・実装した．論理式に変換する際，モデルが含むサブシステムを抽象化したり，安全性と関連するモデル記述をスライシングしたりする方法を検討した．検査は，対象となるサブシステム階層数と信号の長さを調整しながら実施するが，これらの変数の値を反復深化させて検査する方法を検討した．また，38種類のブロック型や多様な連結構造を扱う方法を検討した．（2）モンテカルロ法と（1）の手法を組み合わせたSimulinkモデルの網羅テスト手法について研究した．モンテカルロ法と手法（1）を順次用いる手法を設計・実装した．多様なモデルに対して効果的な両手法の切り替え条件を実験的に求めた．網羅テストに手法（1）を用いる際はテスト項目のリストについて反復的に検査していくが，効率的な処理方法を検討した．（3）（1）と（2）の手法をMATLAB上に実装し，評価実験を行った．大規模複雑なSimulinkモデルの例として，人工的モデルと産業的モデルを約15例収集した．各モデルについて複数の安全性を証明・反証する実験と，網羅テストの実験を実施した．また，既存ツールとの比較実験を実施した．実験結果では，提案手法が正しく効率的に動作することと，実行時間やテスト網羅度について，既存ツールと比較して良好な性能が得られることがわかった．
すべて 2023 2022 その他
すべて 国際共同研究 (1件) 雑誌論文 (3件) (うち国際共著 2件、 査読あり 3件) 備考 (3件)
Proc. 22nd International Conference on Software Quality, Reliability and Security (QRS)
巻: － ページ: 422-433
10.1109/QRS57517.2022.00050
Proc. NASA Formal Methods
巻: 13260 ページ: 733-751
10.1007/978-3-031-06773-0_39
Proc. 23rd International Conference on Formal Engineering Methods (ICFEM)
巻: 13478 ページ: 156-172
10.1007/978-3-031-17244-1_10
https://zenodo.org/record/6387089#.ZC6eQRVBwqs
https://www.gaio.co.jp/products/prompt-2/
https://zenodo.org/record/6781295#.ZC6hrRVBwqs
