Software model checking for real-time properties of embedded assembply program with interruptions

割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の理論と実装の研究を対象として、SMT（Satisfiable Modulo Theories）ソルバーを用いて、抽象化精錬によるソフトウェアモデル検査の実現と評価の研究を行っている。2022年度はおおむね目標通り、以下の（１）組込みアセンブリプログラムのSMTソルバーを用いた抽象化精錬によるソフトウェアモデル検査器の実現、（２）時間模倣関係理論による割込み処理の削減、（３）リアルタイムオペレーティングシステムのスケジューリングの形式的検証、を行った：（１）組込みアセンブリプログラムを対象とした、昨年度までに実現している、SMT定理証明器を用いた、抽象化精錬によるソフトウェアモデル検査器の実装とロボットアセンブリプログラムによる検証実験を行った。現在、理論と実証実験を含めた論文を作成して、ジャーナルへの投稿を準備している。（２）ソフトウェアモデル検査のフロントエンド処理として、時間模倣関係理論をもとに実現した、タイマ割込みを削減する手法を実装して、ソフトウェアモデル検査の効率化を実現した。ロボットアセンブリプログラムを対象に実験的に評価を行った。現在、ジャーナルへの投稿を行った。（３）カーネギーメロン大学とオックスフォート大学の共同開発のSMT/SATによるソフトウェアモデル検査器CBMC（Bounded Model Checker for C and C++ programs）を用いて、名古屋大学で開発・運用しているリアルタイムオペレーティングシステムTOPPERS（Toyohashi Open Platform for Embedded Real-time Systems）のスケジューリングの優先度逆転現象の形式的検証を行い、有効性を実証した。現在、ジャーナルへの投稿を行った。

割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の理論と実装の研究を対象として、SMT（Satisfiable Modulo Theories）ソルバーを用いて、抽象化精錬によるソフトウェアモデル検査の実現と評価の研究を行っている。2022年度はおおむね目標通り、以下の（１）組込みアセンブリプログラムのSMTソルバーを用いた抽象化精錬によるソフトウェアモデル検査器の実現、（２）時間模倣関係理論による割込み処理の削減、（３）リアルタイムオペレーティングシステムのスケジューリングの形式的検証、を行った：（１）組込みアセンブリプログラムを対象とした、昨年度までに実現している、SMT定理証明器を用いた、抽象化精錬によるソフトウェアモデル検査器の実装とロボットアセンブリプログラムによる検証実験を行った。現在、理論と実証実験を含めた論文を作成して、ジャーナルへの投稿を準備している。（２）ソフトウェアモデル検査のフロントエンド処理として、時間模倣関係理論をもとに実現した、タイマ割込みを削減する手法を実装して、ソフトウェアモデル検査の効率化を実現した。ロボットアセンブリプログラムを対象に実験的に評価を行った。現在、ジャーナルへの投稿を行った。（３）カーネギーメロン大学とオックスフォート大学の共同開発のSMT/SATによるソフトウェアモデル検査器CBMC（Bounded Model Checker for C and C++ programs）を用いて、名古屋大学で開発・運用しているリアルタイムオペレーティングシステムTOPPERS（Toyohashi Open Platform for Embedded Real-time Systems）のスケジューリングの優先度逆転現象の形式的検証を行い、有効性を実証した。現在、ジャーナルへの投稿を行った。